From dc5764630fdf34f72bbe76efd4b79d3b2bc3dd40 Mon Sep 17 00:00:00 2001 From: DreamingOfClouds Date: Fri, 23 Oct 2026 08:01:24 -0500 Subject: [PATCH] =?UTF-8?q?Add=20fragmentation-ceiling:=20exact=20=CE=9B?= =?UTF-8?q?=20ship=20threshold=20for=20the=20#4610=20family,=20with=20Lean?= =?UTF-8?q?=20(no=20=CE=BA=20change)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rebuilds the fragmentation loss Λ of the public #4610 word (23.8746264727/call) and the exact threshold Λ* = 23.8536932758 for a +0.05% κ gain; proves helper neutrality, the descent price and the A30-CUT centre bound (Lean, 37 declarations, no sorry), and prices the coded centre-free family against them. Co-Authored-By: Claude Opus 5.5 --- research/fragmentation-ceiling/PROOF.md | 192 +++++++ research/fragmentation-ceiling/README.md | 65 +++ .../data/verify_output.txt | 22 + research/fragmentation-ceiling/lean/Skel.lean | 519 ++++++++++++++++++ .../lean/lake-manifest.json | 117 ++++ .../fragmentation-ceiling/lean/lakefile.toml | 10 + .../fragmentation-ceiling/lean/lean-toolchain | 1 + research/fragmentation-ceiling/verify.py | 205 +++++++ 8 files changed, 1131 insertions(+) create mode 100644 research/fragmentation-ceiling/PROOF.md create mode 100644 research/fragmentation-ceiling/README.md create mode 100644 research/fragmentation-ceiling/data/verify_output.txt create mode 100644 research/fragmentation-ceiling/lean/Skel.lean create mode 100644 research/fragmentation-ceiling/lean/lake-manifest.json create mode 100644 research/fragmentation-ceiling/lean/lakefile.toml create mode 100644 research/fragmentation-ceiling/lean/lean-toolchain create mode 100644 research/fragmentation-ceiling/verify.py diff --git a/research/fragmentation-ceiling/PROOF.md b/research/fragmentation-ceiling/PROOF.md new file mode 100644 index 0000000000..c4033090d7 --- /dev/null +++ b/research/fragmentation-ceiling/PROOF.md @@ -0,0 +1,192 @@ +# Proofs: one number governs the native call + +Status tags used for every claim: + +| tag | meaning | +|---|---| +| **PROVED-LEAN** | machine-checked in `lean/Skel.lean` (Lean 4 + Mathlib, no `sorry`), under the stated hypotheses | +| **PROVED-PAPER** | proof given here, not formalised | +| **CHECKED-EXACT** | exact or 60-digit computation. "verify.py" means it is rebuilt by `verify.py` from the public #4610 package; "source" means it was run in the research notes on data not shipped here | +| **CONDITIONAL** | holds only under a stated modelling assumption, named in its scope | + +Every claim carries its scope. Pointers `[k]` refer to numbered lines of `data/verify_output.txt`. + +Notation. P = `research/joint-helper-lattice/PROOF.md`; Q = `research/kappa-round3-warp-20261022/PROOF.md`; V = that directory's `verify_candidate.py`; NE = `research/kappa-rebuild/complex/native_extensions.py`. "#4610" is the word `kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`, whose κ is in (0.0030217758, 0.0030217759) [8]. + +## 0. Setting + +An invoice is a pair of multisets: credits T and paid jobs P of positive integer ranks. Its moment is f(t) = Σ_T k^t − Σ_P r^t. The pricer returns the first crossing of f in C = 1 − t on (0, 0.05], and f > 0 at small C. Fix a bar and write t* = 1 − bar; the default is bar = 0.0030233 (about 0.05% above κ(#4610)). Because the pricer returns the first crossing, **κ ≥ bar implies f(t*) ≥ 0** with no further assumption. The converse needs f to have a single crossing on (0, 0.05] (assumption S1, checked on a 1000-point grid for the invoices used here). + +**Frames and fields.** A frame is a subspace of F₂⁹. A persistent field carries one logical value in a current frame, from a start frame S_f to a final frame T_f. Events on a field are paid transports E → F (which cost a rank) and free events (warps K_G with G ∈ GL(9,2), and scalar operations). A climb is a nested paid transport E ⊂ F. A field's history is an integer dimension path d₀ = dim S_f, …, d_n = dim T_f with costs c_j ≥ 0. Write R_f = dim T_f − dim S_f. + +**Contract hypotheses (used explicitly).** + +| | statement | source | status | +|---|---|---|---| +| H1 | A field's frame dimension changes only at paid transports. Warps preserve dimension. Scalar operations act inside one frame. | P:15–17; Q:5–8 | package contract. On #4610 all 240 warps preserve dimension and every field replays start → final in both orientations [2] | +| H2 | A nested transport E ⊂ F costs dim F − dim E. A general transport costs dim E + dim F − 2 dim(E ∩ F) ≥ \|dim F − dim E\|, with the parity of dim F − dim E. | nested: P:15, Q:5–6. General formula: L_E ∩ L_F = (E ∩ F) ⊕ (E + F)^⊥ | nested: package contract. General formula: **PROVED-LEAN** (`rankCost_ge_abs`, `rankCost_nested`, `rankCost_parity`) | +| H3 | A helper is credited once, with its whole residual rank R_f = dim T − dim S, S ⊊ T. No duplicate field, discarded helper, clean input or free temporary productive input. | P:19; Q:18–21; V:40 | package contract | +| H4 | Transports of helper and main fields are ascending climbs. | NE:123 | a verifier convention. Section 3 shows the results hold with or without it | +| H5 | Unit (v, d) = (112, 8). One pair per LOCAL, port-uniform. Kap path controller with thick set {0, 2p, odd}, e = 1. | model family | model assumption. The p16 a7 invoice is public [1] | + +The **centre** is the owned rank-8 jobs on the C buffers. In #4610 there are 8 per call (M = 64). + +## 1. Analytic core (PROVED-LEAN) + +For 0 < t ≤ 1 and x ↦ x^t on [0, ∞): + +- **Lemma 1 (subadditivity).** (Σxᵢ)^t ≤ Σxᵢ^t, strictly for 0 < t < 1 when two terms are positive. `rpow_add_le`, `rpow_sum_le`, `rpow_add_lt`, `rpow_sum_lt`. +- **Lemma 2 (chord).** For 0 ≤ x ≤ y: x^t ≥ x·y^{t−1}. `mul_rpow_sub_one_le`. +- **Lemma 3 (exchange).** For 0 ≤ x ≤ y and r ≥ 0: (y+r)^t − y^t ≤ (x+r)^t − x^t. Proof: concavity applied at μ = r/(y−x+r). `rpow_increment_antitone`. + +## 2. Paths, Theorem B and Theorem C + +**Lemma 4 (path identity; PROVED-LEAN).** For an integer path with R = d_n − d₀ and down-mass D = Σ max(−Δ_j, 0): Σ|Δ_j| = R + 2D. Hence under H1–H2, Σ c_j ≥ R + 2D. `FieldPath.sum_abs_eq`, `mass_ge`. + +**Theorem B (per-call decomposition; PROVED-LEAN under H1–H3).** Every paid native job is a single-field climb or a centre job. The native per-call moment φ(t) := Σ_helpers h^t − Σ_paid r^t satisfies + + φ(t) = −2v·d^t − Σ_centre c^t − Λ(t), Λ(t) = Σ_f Λ_f(t), Λ_f(t) = Σ_j c_j^t − R_f^t ≥ 0. + +For 0 < t < 1, Λ_f = 0 iff the field pays a single job of rank R_f (or none if R_f = 0); two positive jobs give Λ_f > 0. Proof: partition the jobs by field; Lemma 4 gives Σ c_j ≥ R_f, then Lemma 1 and monotonicity give Σ c_j^t ≥ R_f^t. `decomposition`, `FieldPath.lam_nonneg`, `lam_pos_of_two`, and for real subspace histories `lam_nonneg_ofSubspaces`. + +*Application to #4610 (CHECKED-EXACT, verify.py).* +- Σ climbs = R_f on all 632 fields, in both orientations [2]. +- Climb profile plus the 8 centre jobs equals the public `local_paid` exactly [2]. +- Λ(t*) = **23.8746264727**: helpers 16.2711462249, mains 7.6034802478 [4]. +- The identity closes to 6·10⁻⁵⁷ [5]. + +**Theorem C (no net-productive helpers; PROVED-LEAN under H1–H3).** For every helper, Hnet_f = Σ c_j − R_f ≥ 0, and its moment contribution R_f^t − Σ c_j^t = −Λ_f ≤ 0, with equality iff it has exactly one climb. A helper is at best neutral whatever its credited rank, so the helper census enters κ only through Λ_h. Crediting descents as well does not change this: credit mass R_f + D against paid mass ≥ R_f + 2D. `hnet_nonneg`, `hnet_inverse_nonneg`, `helper_contribution_nonpos`. + +*Consequence (PROVED-PAPER).* A net-productive helper (Hnet < 0) needs either a free dimension increase (violating H1) or credit for a non-independent input (violating H3). The moment can turn positive only by crediting finer than paying: credit {1,1} against paid {2} gains 2 − 2^t* = 0.0041868 [10]. + +**Lemma 5 (descents never help; PROVED-LEAN for nested endpoints, PROVED-PAPER otherwise).** With endpoints fixed, replacing a field's path by the single transport start → final never raises the paid moment. For nested endpoints (all helpers and mains in the contract) this is exactly Λ_f ≥ 0. For non-nested endpoints it is the triangle inequality of the rank metric, which is outside the verifier's current scope. A single-field exhaustive search (all walks of at most 5 steps, ranks 1–9, dimensions 0–12, 40 digits) agrees: the minimum paid moment is that of the single climb (CHECKED-EXACT, source). Hence H4 is a convention that costs nothing. + +## 3. Descent price (Theorem D) + +**Theorem D (PROVED-LEAN under H1, H2).** A field with fixed endpoints, R ≥ 0, and one descent of rank r has + + Λ_f(t) ≥ r^t + (R+r)^t − R^t ≥ r^t + (9+r)^t − 9^t (second step for R ≤ 9). + +Proof: the descent step pays ≥ r; the other steps telescope to R + r (Lemma 4), so by Lemma 1 their moment is ≥ (R+r)^t; the second inequality is Lemma 3. `descent_price`, `descent_price_nine`. + +At t* [9] (CHECKED-EXACT, verify.py): the bound is 1.99022 (r = 1), 3.97594 (r = 2), 5.95983 (r = 3), 7.94244 (r = 4). Corollary: any word with Λ ≤ Λ* contains at most ⌊Λ*/1.99022⌋ = **11** rank-1 descents. + +*Order of magnitude (PROVED-PAPER).* A descent costs first order in mass (about 2r). Any unlock of fragmentation is a concavity gain, second order in 1 − t (about 0.003 per unit of mass). + +*Application to #4610 (CHECKED-EXACT, source; not rebuilt by verify.py).* With the scalar program fixed, relaxing the frame model so that all 44 frame-infeasible helpers are free gains at most 1.3293 + 0.1176 of Λ, below the price 1.9902 of one descent. A relaxation freeing the hub field 225 completely gains 0.07417 against that price, net −1.916 per call. These are relaxation bounds, and are scoped to a fixed scalar program with nested descents only (CONDITIONAL on that scope). + +## 4. Theorem A and the exact ship threshold + +**Theorem A (controller separation; PROVED-PAPER, CHECKED-EXACT at p16 a7 by verify.py).** Under H5, f(t) = (p+2)·φ(t) + Γ_{p,a}(t), where Γ depends on the controller only: targets 2v at 1 + d(p+2) and 2v at 1 + d(j+1) for j = 1..a and j = 1..b (b = p−1−a); paid v(p−1) rank-1 thin shears and 2v at d(j+1) for the same j. This is the invoice construction itself. Public check [1]: at (16, 7), with (H, N) from `ARITHMETIC.json`, it reproduces `targetMoment` and `paidMoment` of `NumericalMoments.lean` coefficient by coefficient (13 target and 14 paid terms). + +**Corollary A1 (universal controller; CHECKED-EXACT for p ≤ 400 plus PROVED-PAPER tail, verify.py; CONDITIONAL on the kap family).** Define φ* = −max_{p,a} Γ_{p,a}(t*)/(p+2). Over all p ≥ 1 and all a the maximum is at p = 16, a ∈ {7, 8} (the same invoice): φ* = **−1868.2220388492** [7], [7b]. For p ≤ 400 this is an exact search. For p > 400, write Γ/(p+2) = F(p) + Σ_{k=1}^{p−1}(2v·δ_{j_k} − v)/(p+2) with F(p) = 2v(1+d(p+2))^t/(p+2), which decreases in p, and δ_j = (1+d(j+1))^t − (d(j+1))^t ≤ δ_1 (Lemma 3), each bracket positive; so Γ/(p+2) ≤ F(401) + 2vδ_1 − v = 1858.7424 < −φ* [7b]. In the family, some (p, a) clears the bar with native call φ only if φ(t*) ≥ φ*, and under S1 also if. + +**Theorem (ship threshold).** Under H1–H5 and the #4610 centre (8 rank-8 jobs per call): + + κ ≥ bar ⟹ Λ(t*) ≤ **Λ\* = −φ\* − 232·8^{t\*} = 23.8536932758.** + +PROVED-PAPER from Theorem B, Theorem A and the first-crossing remark in §0. The converse holds under S1 (CONDITIONAL). For #4610 [6]: + +- Λ − Λ* = **0.0209331969 per call**. +- 18(Λ* − Λ) = −0.3767975440, which equals the public invoice f(t*) to 10⁻⁴⁰. This closes the whole chain independently. +- At #4610's own root t₀ = 1 − κ, Λ(t₀) = Λ*(bar = κ) = 23.8626369199 to 10⁻⁴⁰ [12]. + +**Exchange values per call at t\*** (CHECKED-EXACT, verify.py [10]; the gap to close is 0.0209332): + +| move | value | +|---|---| +| merge two rank-1 climbs on one field (1+1 → 2) | 0.0041868 (5 per call clear the bar) | +| uneven split 4+4 → 3+5 (the #4610 mechanism) | 0.00075844 | + +*Scope.* The threshold applies to words in the family 𝔉: the kap path controller at unit (112, 8) with the 8-job centre. It says nothing about other units, other controllers outside the kap family, or words that change H1–H3. + +## 5. A30-CUT: the owned centre is moment-optimal + +**Setting.** H1–H3, linear contents over any field, U uses of the centre. Each use must deliver a vector whose p-part is c_u·p_u. Write g(x) = x^t and y = g(8)/8. + +**Hypotheses.** +- **P-ATOM (contact restriction).** Carriers acquire p-content only by reading the port, and no new L–L contacts are added. Relative to the frozen L word, p_u is then an atomic item independent of all other carrier content. This is a modelling step; in real coordinates it needs the lemma that with no L–L contacts every carrier's content lies in span(its own native input, port reads received). +- **DELIV.** Every add that changes an L register's p-coefficient happens at frame 0. In the variant ψ there is one port frame P and the adds happen at frames F with F ∩ P = 0. +- **Mains are net-up.** True for #4610 (starts are lines in P and finals are pinned at dimension 8). Without it the dual fails: a credited 8 → 0 field that need not end holding its own input gives −7.95. + +**Theorem (A30-CUT).** Σ_fields [Σ_jobs g(c_j) − g(credit_f)] ≥ U·g(8) + Σ_f slack_f with every slack_f ≥ 0. Fields with no centre traffic keep slack_f = Λ_f. The number of owned, helper, main and target registers, dirty contents, inverse credit, sharing across uses and order are arbitrary. + +*Proof.* Take φ = dim (or ψ = dim(· ∩ P)); both are integer-valued and 1-Lipschitz for rank. + +1. **(i) Cut lemma (PROVED-PAPER, CONDITIONAL on P-ATOM and DELIV).** For a level λ ∈ {1..8} let N_λ = span{r_j : φ(S_j) < λ}. By induction over events, every content held below λ lies in N_λ plus the vectors moved by transports that crossed λ downward. At the end, below λ sit the U delivered vectors and the r_j of every helper with φ(S_j) ≥ λ > φ(T_j); by P-ATOM these are independent modulo N_λ. Each crossing transport moves one field's content, so downward crossings at λ number at least U + (net-down helpers at λ). +2. **(ii) Per-level telescoping (PROVED-LEAN).** On each field, up(λ) − down(λ) = [λ ≤ final] − [λ ≤ start]. `FieldPath.up_sub_dn`. Summing (i) over fields and levels gives Σ_f cov_f ≥ 8U, where cov_f = Σ_{λ=1..8} min(up, down) (owned fields: down). +3. **(iii) Rank pays for crossings (PROVED-LEAN).** A job crosses at most min(c_j, 8) of the levels 1..8. `levels_crossed_le`, `crossings_le_mass`. +4. **(iv) Dual feasibility of y (PROVED-LEAN for each case given Σ c_j ≥ R + 2k; that mass bound is PROVED-PAPER; k ≥ 2 case for t ∈ [0.99, 1]).** We need loss_f ≥ y·cov_f on every field. + - Owned fields: g(a) ≥ y·min(a, 8) by Lemma 2 (`owned_dual`). + - Credited fields with cov = 0: loss = Λ_f ≥ 0. + - Credited fields with k = cov ≥ 1: levels 1..8 give Σ c_j ≥ R − 1 + 2k and parity makes it Σ c_j ≥ R + 2k (`rankCost_parity` per step; the summation of parity along the path is PROVED-PAPER, not in Lean). For k = 1, Lemmas 1 and 3 give loss ≥ 1 > y (`credited_k1`, `y_lt_one`). For k ≥ 2, Lemma 2 with y = 9 and Bernoulli (9^{t−1} ≥ 25/27 for t ≥ 0.99) give loss ≥ y·k (`credited_k2`, `nine_rpow_sub_one_ge`). + - The owned 8 → 0 job attains the bound, so it is tight. + +At t*: y = 0.993733 and 9^{t−1} = 0.993379 [11]. ∎ + +**Corollaries (CONDITIONAL on the hypotheses above).** +1. No dirty, inverse-credited, catalytic or shared centre gets below g(8) = 7.9499 per use. +2. Recruiting an existing helper or main as a carrier costs slack ≥ 0.9968 (minimum at path 1 → 0 → 9; CHECKED-EXACT, source, on all dimension paths of at most 6 jobs, see below), while the largest baseline Λ_f in #4610 is 0.05959 [11]. Any gain must therefore come from fields with no centre traffic, which is Λ. + +*Independent checks (CHECKED-EXACT, source).* An exhaustive Dijkstra over all subspace states of F₂ⁿ and F₃ⁿ (n = 3, 4; helpers, owned registers, inverse credit on or off, one or two uses) found no pattern below the owned centre. An independent re-derivation checked dual feasibility on all 5,978,700 dimension paths of at most 6 jobs (minimum reduced cost 0, no violations; smallest credited traffic slack 0.99682), and on real-subspace ψ models (19,558,506 and 13,017,840 paths). + +**Scope not covered.** Cross-use sharing with different ports and deliveries at a common frame z; deliveries at frames meeting P; dropping P-ATOM (the decoder question); carriers that ride warps; query shears. + +## 6. Centre-free (coded) family: exact budget and ceiling + +Context. #4929 (Dugongue) is a centre-free producer with an explicit code A = I − 14P. #4694 and #4698 (Cinna Davis, 1337isnot1337) supply a 640-field interface, +112 cache pricing and eight chains. #4933 (dillona) is a coded p16 caller with deferred decoding. #4932 and #4931 (Clear1nsight) give a one-bank decoder ceiling and a one-port prefix offer. #4940 (SethBurkart123) proposes A⁻¹-mixed query shears. This section prices these constructions in the Λ currency. Claims about their contents are as stated in those PRs and were not re-run here. + +**6.1 The coded endpoint is #4610 with the centre deleted (CHECKED-EXACT, source, on #4929's SOURCE-WORD).** Same 3290 climbs, same Λ (helpers 16.2711462249, mains 7.6034802478), same 632 start and final frames, in both orientations; the difference is 6,596 free dyadic adds. + +**6.2 Exact budget (CHECKED-EXACT, verify.py [13]).** With φ_coded = φ(#4610) + 8·8^{t*}: + + B = φ_coded − φ* = **63.577975271157 per call** = 8f(8) − (Λ − Λ*), where f(8) = 8^{t*} and 8f(8) = 63.5989084680. + +Over the 18 calls of the invoice, 18B = 1144.40355488. Any adapter that restores the contract endpoint must therefore cost less than 8f(8) − 0.0209332 per call. + +**6.3 Per-call restoration (CONDITIONAL on A30-CUT scope).** The repair ΔY = 14PX is exactly the source's eight centre deliveries (22 Y targets per port; 24 distinct needed vectors). A30-CUT applies under its hypotheses: DELIV and mains net-up hold here (p_u is read at a port register of dimension 8, mains are net-up, deliveries are at frame 0), and P-ATOM is assumed for the adapter. Then the cost is ≥ 8f(8) = 63.5989 > B, short by exactly 0.0209331969. The deleted centre is the cheapest in-scope adapter, and coded + adapter ≤ κ(#4610). + +Cheapest designs priced (CHECKED-EXACT, source): owned centre re-instated 63.5989 (margin −0.0209); hub at line 114/115 (in all ports) 63.6715; hub at a dim-2 meet 63.7072; #4694 direct cache 112; post-call up-and-down 224. + +**6.4 Single-commodity lemma at any frame and time (CHECKED-EXACT, source; SUBCLASS: owned carriers, fixed #4610 main chains, no warp-riding carriers, no target-to-target relays).** If every carrier holds a multiple of one p_u and deliveries are at any frame the target occupies after p_u exists, each use costs ≥ f(8). Proof: if some target is served at frame 0, the content path from P_u to 0 has total rank ≥ 8, so cost ≥ f(8) by Lemma 1. Otherwise the 22 targets need ≥ h_u distinct nonzero arrival frames, each costing ≥ 1; exact hitting-set MILPs give h_u = 16, 16, 16, 16, 14, 18, 14, 18, all ≥ 14 > f(8). Nested stops with shedding at a common frame M ⊆ K (K the intersection of the 8 ports, dimension 5) were checked on all 31 lines of K against all 203,360 (line, hyperplane) pairs: no design gives every late target a nested stop. + +**6.5 Deferred decoding (#4933).** The budget becomes whole-invoice: 18B = 1144.4036, i.e. at most 71.5252 per negative bank if the positive half is free (CHECKED-EXACT, verify.py [13]). +- (CONDITIONAL: P-ATOM, owned carriers, fixed main chains.) Decoding one stage-s factor means delivering 8 independent items. At the stage this is the per-call adapter, so ≥ 8f(8) by A30-CUT. Later or post-hoc, items of different debt classes are independent modulo N_λ, so the count adds over the **53** debt classes (class counts EXACT on #4933's `GAUGE.json`): 53·8f(8) = 3370.74. +- Any mix of at-stage and later decoding costs ≥ 18·8f(8) = 1144.78035 against 1144.40355, a shortfall of 18 × 0.0209332 = 0.376798 (CONDITIONAL: P-ATOM, owned carriers, fixed main chains). Reinstating all 144 centre calls attains it and is #4610. +- #4932's one-bank decoder needs ≥ 112 grade-2 channels per bank, 112f(2) = 223.53. Its grade-2 projection is block-diagonal over independent banks, so 16 banks cost 3576.5 against 1144.40 (scope: the single-layer decoders that #4932 treats). +- #4931's one-port prefix offer costs +0.0057610 per use with no reward in the moment. +- Past the invoice, handing codes to the parent recursion is not allowed by the current compiler (#4933's own README); that would need a typed recursive coded product. + +**6.6 A⁻¹-mixed query shears (#4940).** Frame replay on #4929's canonical frames (CHECKED-EXACT, source): the 112 x-roles enter their calls at 112 distinct non-nested dimension-1 lines, so a cross-port add at the call entrance fails the verifier's scalar-source-frame rule, and each source must first leave its line by a paid rank-1 transport: ≥ 112 rank-1 jobs per thick call. Commutation (CHECKED-EXACT, F₂-symplectic, all 5,824 coupled pairs): in the physical ABI of #4933 the code C = K⁻¹AK does not commute with Q, so the needed input conversion QCQ⁻¹ is non-monomial. The sub-lemma that one boundary conversion per thick call is Q-twisted is PROVED-PAPER for conversions inside the stage-s recode group, and argued for common-frame conversions (CONDITIONAL). Priced in #4940's own invoice, break-even is about 63.6 per call and the repair costs ≥ 112, so there is no root at any p (CONDITIONAL on the Q-twist sub-lemma above); the model reproduces #4940's published 0.0030201659770. The credit for #4940 is the idea and its exact diagonalisation: with it the question reduces to the same centre budget B. + +**6.7 What reopens the coded route (stated as scope, not as a claim).** Every statement in 6.3–6.6 is inside the A30-CUT and single-commodity scope. Doors outside it, shared with #4610 without any coding: network-coded carriers with stops and shedding; decoders that read X directly (breaking P-ATOM); a native word with port-independent entrance lines. + +## 7. Claim index + +| claim | tag | rebuilt by verify.py | +|---|---|---| +| Lemmas 1–3 | PROVED-LEAN | text check only | +| H2 for subspaces (general formula, nested, parity) | PROVED-LEAN | | +| Lemma 4, Theorem C | PROVED-LEAN | | +| Theorem B: identity, Λ_f ≥ 0, strictness | PROVED-LEAN | | +| Theorem B on #4610 (Λ = 23.8746264727, identity to 10⁻⁵⁷) | CHECKED-EXACT | yes [2]–[5] | +| Lemma 5 (nested endpoints) | PROVED-LEAN | | +| Lemma 5 (non-nested); inverse-credit remark | PROVED-PAPER | | +| Theorem D, descent price table, cap of 11 | PROVED-LEAN; numbers CHECKED-EXACT | yes [9] | +| Descent unlock bounds on #4610 (44 helpers, hub 225) | CHECKED-EXACT, scoped to fixed scalar program | no | +| Theorem A, p16 a7 invoice | PROVED-PAPER; CHECKED-EXACT | yes [1] | +| Corollary A1 (best controller in the kap family, all p) | CHECKED-EXACT (p ≤ 400) + PROVED-PAPER tail; CONDITIONAL on the family | yes [7], [7b] | +| Ship threshold Λ\* = 23.8536932758, gap 0.0209331969 | PROVED-PAPER (necessity); CHECKED-EXACT numbers | yes [6] | +| Sufficiency of Λ ≤ Λ\* | CONDITIONAL on S1 | no | +| A30-CUT (ii), (iii), (iv) | PROVED-LEAN; in (iv) the parity summation Σ c_j ≥ R + 2k is PROVED-PAPER | | +| A30-CUT (i) cut lemma | PROVED-PAPER, CONDITIONAL on P-ATOM, DELIV, mains net-up | | +| A30-CUT exhaustive and independent dual checks | CHECKED-EXACT | no | +| Coded budget B = 63.577975271157, 18B, 71.5252, shortfall | CHECKED-EXACT | yes [13] | +| Coded endpoint equals #4610 minus centre | CHECKED-EXACT | no (needs #4929 data) | +| Per-call and deferred kills (6.3–6.5) | CONDITIONAL on A30-CUT scope (P-ATOM, DELIV, mains net-up) and, for 6.4–6.5, owned carriers and fixed main chains; counts CHECKED-EXACT | no | +| #4940 no-root conclusion (6.6) | CONDITIONAL on the Q-twist sub-lemma | no | +| #4940 frame and commutation witnesses | CHECKED-EXACT | no (needs #4940 data) | + +## 8. Lean build + +`lean/Skel.lean` imports only Mathlib. It builds with the shipped `lean/lakefile.toml` and `lean/lake-manifest.json` (Lean `v4.33.0-rc1`, pinned Mathlib): `cd lean && lake exe cache get && LEAN_NUM_THREADS=4 lake build Skel`, with "Build completed successfully". `#print axioms` on the headline theorems gives only `propext`, `Classical.choice`, `Quot.sound`. Not formalised: the cut lemma (i), the identification of verifier events with `FieldPath`s (that is H1–H3, checked on #4610 by `verify.py`), the invoice structure, S1, and the real-number constants at t*. diff --git a/research/fragmentation-ceiling/README.md b/research/fragmentation-ceiling/README.md new file mode 100644 index 0000000000..236e94ea25 --- /dev/null +++ b/research/fragmentation-ceiling/README.md @@ -0,0 +1,65 @@ +# Fragmentation loss: one number governs the native call + +**No κ change. This package does not add a word.** It gives an exact test for any word in the #4610 family, and prices the centre-free (coded) constructions against it. + +TL;DR. For a word in the kap family at unit (112, 8) with the 8-job rank-8 centre, κ ≥ 0.0030233 requires + + Λ(t\*) ≤ Λ\* = **23.8536932758** per call, + +where Λ(t) = Σ over fields of (Σ climbs c^t − R_f^t) is the *fragmentation loss* and t\* = 1 − 0.0030233. The #4610 word has Λ = 23.8746264727, so it is **0.0209331969 per call** (0.088% of Λ) above the threshold. Equivalently the public invoice is at f(t\*) = −0.3767975440 = 18 × the gap. Λ is exact, linear in the climb profile, and needs no κ solve. + +## What is in the package + +| file | content | +|---|---| +| [PROOF.md](PROOF.md) | definitions, hypotheses, every theorem with a status tag (PROVED-LEAN / PROVED-PAPER / CHECKED-EXACT / CONDITIONAL) and its scope | +| [verify.py](verify.py) | stdlib-only script, about 10–15 s: rebuilds Λ, the identity φ = −2v·d^t − centre − Λ, the threshold Λ\*, the descent prices and the coded-family budget from #4610's public package | +| [data/verify_output.txt](data/verify_output.txt) | its output, `ALL CHECKS PASSED` | +| [lean/Skel.lean](lean/Skel.lean), `lean/lean-toolchain`, `lean/lakefile.toml`, `lean/lake-manifest.json` | Lean 4 + Mathlib (pinned): 37 theorem/lemma declarations, no `sorry` | + +## Results + +1. **Λ decomposition (Theorem B).** φ(t) = −2v·d^t − Σ_centre c^t − Λ(t), with Λ_f ≥ 0 and Λ_f = 0 iff the field pays one climb of rank R_f. PROVED-LEAN; exact on all 632 fields of #4610. +2. **Theorem C.** No helper is net-productive: its moment contribution is −Λ_f ≤ 0 for every credited rank. PROVED-LEAN. +3. **Exact ship threshold.** Λ\* = 23.8536932758; p = 16, a = 7 is the best controller in the kap family for every native call (CHECKED-EXACT for p ≤ 400, with a proved bound for p > 400). One 1+1 → 2 merge is worth 0.0041868 per call; five per call would clear the bar. +4. **Descents never help (Lemma 5) and have an exact price (Theorem D).** A rank-r descent costs at least r^t + (9+r)^t − 9^t: 1.99022 for r = 1, so at most 11 descents fit under Λ\*. PROVED-LEAN. +5. **A30-CUT.** Under the stated contact hypotheses the owned centre is moment-optimal: every use costs at least 8^t\* = 7.9499, whatever the carriers, inverse credit or sharing. PROVED-LEAN (dual, with the parity summation on paper) plus PROVED-PAPER (cut lemma), CONDITIONAL on P-ATOM, DELIV and mains net-up. +6. **Coded centre-free family.** The coded endpoint is #4610 with its centre deleted, so its exact per-call budget is B = 8·8^t\* − 0.0209332 = 63.577975271157. Per-call and deferred repairs cost at least 8·8^t\* per stage in scope, short by exactly the #4610 gap (18 × 0.0209332 = 0.376798 over the invoice). CONDITIONAL on the A30-CUT scope (P-ATOM, DELIV, mains net-up; owned carriers and fixed main chains for the deferred case); see PROOF.md section 6. + +## Reproduce + +From a checkout containing the public #4610 package: + +```sh +python3 -B research/fragmentation-ceiling/verify.py [PKG_ROOT] [BAR] +``` + +`PKG_ROOT` is the directory that contains `research/kappa-round3-warp-20261022/` (found automatically when this directory sits next to it, or via `$INTMULT_PKG`). `BAR` defaults to 0.0030233; any other bar changes t\* and so Λ\*, and the script reports the corresponding values. It reads only `ACTUAL-WORD.json.gz`, `ARITHMETIC.json` and `NumericalMoments.lean` of that package, and uses Python's `decimal` at 60 digits. + +Lean (optional): `cd research/fragmentation-ceiling/lean && lake exe cache get && LEAN_NUM_THREADS=4 lake build Skel`. The lakefile pins the Mathlib revision; with the Mathlib cache the build compiles only `Skel.lean` (a few minutes). The `#print axioms` lines at the end of the file report `propext`, `Classical.choice`, `Quot.sound` only. + +## Scope and caveats + +- The threshold is for words in the family: kap path controller (A17 e = 1, thick set {0, 2p, odd}), unit (v, d) = (112, 8), centre of 8 rank-8 jobs per call. It is necessary for every such word; sufficiency assumes the invoice has a single crossing in (0, 0.05] (checked on a grid for the invoices used). +- H1–H3 (frame dimension changes only at paid transports; transport rank; credit once) are the package's own contract (see PROOF.md section 0 for line citations). H2 for non-nested transports is derived, not a contract line. +- "Mains are net-up" and P-ATOM are hypotheses of A30-CUT. Open scope: cross-use sharing at a common frame, deliveries at frames meeting the port, decoders that break P-ATOM, carriers that ride warps, query shears. +- Statements about #4929, #4933, #4932, #4931, #4940 and #4694/#4698 rest on those PRs' published data as fetched, and were priced here; their authors' claims were not re-run. +- The numbered constants in PROOF.md that are marked "source" were computed in research notes from data that is not shipped here; `verify.py` rebuilds the others. + +## Open next questions + +- A word in this family clears +0.05% only if Λ(t*) ≤ 23.8537 per call (gap 0.0209 to #4610). Which scalar-program changes can merge enough climbs? Edits to #4610's fixed program have not produced any so far. +- Can a decoder for P112 that uses gather/scatter-interleaved (staircase) atoms cost below 64? Atoms that beat the masked price exist, so the single-wire decoder wall does not cover them. +- Does A30-CUT extend to cross-use sharing at a common frame, to deliveries at frames meeting the port, and to warp-riding carriers? + +## Credits + +- **Cao Yifan (intqwq), #4610**: the round-three word, its verifier, the contract (P, Q, V) and the public invoice that everything here is computed from. +- **Dugongue, #4929**: the centre-free producer and the explicit code A = I − 14P. +- **Cinna Davis (1337isnot1337), #4694, #4698, #4470**: the 640-field interface, +112 cache pricing, eight chains, and the kap controller lineage. +- **dillona, #4933**: the coded p16 caller, deferred negative banks, `GAUGE.json` identities and the physical ABI of the coded call. +- **Clear1nsight (Chris R), #4931, #4932**: the one-bank grade-2 ceiling and the prefix offer. +- **SethBurkart123 (Cayden Burkart), #4940**: the controller-conjugation idea and its exact diagonalisation. +- zxv and the earlier lineage of the kap family. + +Written by Claude Opus 5.5 (Anthropic), via Claude Code. diff --git a/research/fragmentation-ceiling/data/verify_output.txt b/research/fragmentation-ceiling/data/verify_output.txt new file mode 100644 index 0000000000..02e0209149 --- /dev/null +++ b/research/fragmentation-ceiling/data/verify_output.txt @@ -0,0 +1,22 @@ +[1] kap-family formula at p16 a7 reproduces the public Lean invoice exactly: 13 target and 14 paid coefficients +[2] forward: 632 fields replay start->final; all climbs nested, rank = dim gap; sum climbs = R_f on all fields; climb profile + 8 centre jobs = ARITHMETIC local_paid; centre events 8 +[2] backward: 632 fields replay start->final; all climbs nested, rank = dim gap; sum climbs = R_f on all fields; climb profile + 8 centre jobs = ARITHMETIC local_paid; centre events 8 +[3] mains: 224 fields with R_f = 8; helpers: 408 fields with R_f census = local_helpers {4: 28, 7: 7, 8: 47, 9: 326} +[4] forward: Lambda(t*) = 23.8746264727 (helpers 16.2711462249, mains 7.6034802478) +[4] backward: Lambda(t*) = 23.8746264727 (helpers 16.2711462249, mains 7.6034802478) +[5] phi(t*) = -1868.2429720461; -2v d^t* - 8*8^t* - Lambda = -1868.2429720461; residual -6.00E-57 +[6] p16 a7: phi* = -Gamma(t*)/18 = -1868.2220388492; Lambda* = -phi* - 232*8^t* = 23.8536932758 + Lambda(#4610) - Lambda* = 0.0209331969 per call; 18*(Lambda*-Lambda) = -0.3767975440; public invoice f(t*) = -0.3767975440 +[7] max over kap family p=3..60, all a: Gamma/(p+2) best at p=16 a=8 (phi* = -1868.2220388492); p16 a7 is the max (a and p-1-a give the same invoice): True +[7b] exact max over p=1..400: p=16 a=8; tail bound for p>400: 1858.7424 < 1868.2220: True +[8] public invoice root kappa = 0.0030217758708 (package: in (0.0030217758, 0.0030217759)) +SHIP TEST: a word in this family clears the bar iff Lambda(t*) <= 23.8536933 ; #4610 has 23.8746265 +[9] descent price lower bound r^t+(9+r)^t-9^t: r=1: 1.99022, r=2: 3.97594, r=3: 5.95983, r=4: 7.94244 ; max rank-1 descents with Lambda <= Lambda*: 11 +[10] merge values: 1+1->2 0.0041868 4+4->3+5 0.00075844 needed per call 0.0209332 +[11] A30 dual: y = 8^t/8 = 0.993733 9^(t-1) = 0.993379 max_f Lambda_f = 0.05959 +[12] at its own root t0 = 1 - kappa: Lambda(t0) = 23.8626369199, Lambda*(bar=kappa) = 23.8626369199, difference 1.57E-40 +[13] centre-free budget B = phi_coded - phi* = 63.577975271157 per call = 8 f(8) - gap = 63.577975271157; 8 f(8) = 63.5989084680 + whole invoice 18B = 1144.40355488; 144 f(8) = 1144.78035242; shortfall 144 f(8) - 18B = 0.3767975440 = 18 x gap + per negative bank if the positive half is free: 18B/16 = 71.5252221801; 53 debt classes x 8 f(8) = 3370.74; 16 banks x 112 f(2) = 3576.5 +[14] lean/Skel.lean: 37 theorem/lemma declarations; "sorry" present: False; "axiom" present: False +ALL CHECKS PASSED diff --git a/research/fragmentation-ceiling/lean/Skel.lean b/research/fragmentation-ceiling/lean/Skel.lean new file mode 100644 index 0000000000..d3259363ca --- /dev/null +++ b/research/fragmentation-ceiling/lean/Skel.lean @@ -0,0 +1,519 @@ +import Mathlib + +/-! +# Skel: the combinatorial / analytic cores of the fragmentation-loss theory + +Companion to `PROOF.md`. Everything here is stated for a generic exponent +`t` (usually `0 < t < 1`); the shipped invoice uses `t* = 1 - 0.0030233`. + +* §1 `x ↦ x^t` on `[0,∞)`: subadditivity (finite sums), strict subadditivity, + `x ↦ x^(t-1)` antitone consequences, and the two-point exchange (majorization) lemma. +* §2 Rank formula (H2) for subspaces: `dim E + dim F - 2 dim (E ⊓ F) ≥ |dim F - dim E|`, parity. +* §3 Field paths (H1+H2): telescoping, `paid mass = R + 2·(down mass)`, Theorem C (mass and + moment), the fragmentation loss `Λ_f ≥ 0`, and strict positivity with two climbs. +* §4 Theorem B: the per-call decomposition identity. +* §5 Descent price: `Λ_f ≥ r^t + (R+r)^t - R^t ≥ r^t + (9+r)^t - 9^t`. +* §6 A30-CUT: level crossings (each job's rank ≥ levels it crosses; per-level telescoping) + and dual feasibility of `y = 8^t/8` for owned fields and credited fields. + +Not formalised (paper only): the linear-algebra cut lemma of A30-CUT (independence of the +delivered port vectors modulo `N_λ`), and the identification of the verifier's events with +`FieldPath`s (that is the contract H1–H3, checked on the #4610 word by `verify.py`). +-/ + +open Finset + +namespace Skel + +/-! ## §1 The analytic core -/ + +section Analytic + +variable {t : ℝ} + +/-- Two-term subadditivity of `x ↦ x^t` for `0 ≤ t ≤ 1`. -/ +theorem rpow_add_le {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : + (a + b) ^ t ≤ a ^ t + b ^ t := by + lift a to NNReal using ha + lift b to NNReal using hb + exact_mod_cast NNReal.rpow_add_le_add_rpow a b ht0 ht1 + +/-- Finite subadditivity: `(Σ xᵢ)^t ≤ Σ xᵢ^t` for `0 < t ≤ 1` and `xᵢ ≥ 0`. -/ +theorem rpow_sum_le {ι : Type*} (s : Finset ι) (x : ι → ℝ) (hx : ∀ i ∈ s, 0 ≤ x i) + (ht0 : 0 < t) (ht1 : t ≤ 1) : (∑ i ∈ s, x i) ^ t ≤ ∑ i ∈ s, x i ^ t := by + classical + induction s using Finset.induction_on with + | empty => simp [Real.zero_rpow ht0.ne'] + | insert a s ha ih => + rw [sum_insert ha, sum_insert ha] + have hxa : 0 ≤ x a := hx a (mem_insert_self a s) + have hxs : ∀ i ∈ s, 0 ≤ x i := fun i hi => hx i (mem_insert_of_mem hi) + have h1 := rpow_add_le hxa (sum_nonneg hxs) ht0.le ht1 + linarith [ih hxs] + +/-- `x^t = x · x^(t-1)` for `x > 0`. -/ +theorem rpow_eq_mul_rpow_sub_one {x : ℝ} (hx : 0 < x) : x ^ t = x * x ^ (t - 1) := by + rw [Real.rpow_sub_one hx.ne']; field_simp + +/-- Chord bound from `x ↦ x^(t-1)` antitone: `x · y^(t-1) ≤ x^t` for `0 ≤ x ≤ y`, `t ≤ 1`. -/ +theorem mul_rpow_sub_one_le {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) (ht1 : t ≤ 1) (ht0 : 0 < t) : + x * y ^ (t - 1) ≤ x ^ t := by + rcases hx.eq_or_lt with h | h + · subst h; simp [Real.zero_rpow ht0.ne'] + · rw [rpow_eq_mul_rpow_sub_one h] + exact mul_le_mul_of_nonneg_left (Real.rpow_le_rpow_of_nonpos h hxy (by linarith)) h.le + +/-- Strict two-term subadditivity for `0 < t < 1` and `a, b > 0`. -/ +theorem rpow_add_lt {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (ht1 : t < 1) : + (a + b) ^ t < a ^ t + b ^ t := by + have hab : 0 < a + b := by linarith + have h1 : (a + b) ^ (t - 1) < a ^ (t - 1) := + Real.rpow_lt_rpow_of_neg ha (by linarith) (by linarith) + have h2 : (a + b) ^ (t - 1) < b ^ (t - 1) := + Real.rpow_lt_rpow_of_neg hb (by linarith) (by linarith) + rw [rpow_eq_mul_rpow_sub_one hab, rpow_eq_mul_rpow_sub_one ha, rpow_eq_mul_rpow_sub_one hb] + nlinarith [mul_lt_mul_of_pos_left h1 ha, mul_lt_mul_of_pos_left h2 hb] + +/-- Strict finite subadditivity: two positive terms make `(Σ x)^t < Σ x^t`. -/ +theorem rpow_sum_lt {ι : Type*} [DecidableEq ι] (s : Finset ι) (x : ι → ℝ) + (hx : ∀ i ∈ s, 0 ≤ x i) {i k : ι} (hi : i ∈ s) (hk : k ∈ s) (hik : i ≠ k) + (hxi : 0 < x i) (hxk : 0 < x k) (ht0 : 0 < t) (ht1 : t < 1) : + (∑ j ∈ s, x j) ^ t < ∑ j ∈ s, x j ^ t := by + have hk' : k ∈ s.erase i := mem_erase.mpr ⟨hik.symm, hk⟩ + have hxe : ∀ j ∈ s.erase i, 0 ≤ x j := fun j hj => hx j (mem_of_mem_erase hj) + have hB : x k ≤ ∑ j ∈ s.erase i, x j := single_le_sum hxe hk' + rw [← add_sum_erase s x hi, ← add_sum_erase s (fun j => x j ^ t) hi] + have h1 := rpow_add_lt hxi (lt_of_lt_of_le hxk hB) ht1 (t := t) + have h2 := rpow_sum_le (s.erase i) x hxe ht0 ht1.le + linarith + +/-- Two-point exchange (majorization): for `x ≤ y` and `r ≥ 0`, +`(y+r)^t - y^t ≤ (x+r)^t - x^t`. Equivalently `x^t + (y+r)^t ≤ (x+r)^t + y^t`. -/ +theorem rpow_increment_antitone {x y r : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) (hr : 0 ≤ r) + (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (y + r) ^ t - y ^ t ≤ (x + r) ^ t - x ^ t := by + rcases (add_nonneg (sub_nonneg.mpr hxy) hr).eq_or_lt with hL | hL + · have hr0 : r = 0 := by linarith [sub_nonneg.mpr hxy] + have hy : y = x := by linarith [sub_nonneg.mpr hxy] + subst hr0; subst hy; simp + set L := y - x + r with hLdef + set μ := r / L with hμ + have hμ0 : 0 ≤ μ := div_nonneg hr hL.le + have hμ1 : μ ≤ 1 := by rw [hμ, div_le_one hL]; linarith + have hc := (Real.concaveOn_rpow ht0 ht1).2 + have hxI : x ∈ Set.Ici (0 : ℝ) := hx + have hyrI : y + r ∈ Set.Ici (0 : ℝ) := by simp only [Set.mem_Ici]; linarith + have e1 : (1 - μ) • x + μ • (y + r) = x + r := by + simp only [smul_eq_mul]; rw [hμ]; field_simp; ring + have e2 : μ • x + (1 - μ) • (y + r) = y := by + simp only [smul_eq_mul]; rw [hμ]; field_simp; ring + have c1 := hc hxI hyrI (by linarith : 0 ≤ 1 - μ) hμ0 (by ring) + have c2 := hc hxI hyrI hμ0 (by linarith : 0 ≤ 1 - μ) (by ring) + rw [e1] at c1; rw [e2] at c2 + simp only [smul_eq_mul] at c1 c2 + linarith + +end Analytic + +/-! ## §2 The rank formula (H2) -/ + +section Rank + +variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V] + +/-- Paid rank of a transport `E → F` (P:15): `dim E + dim F - 2 dim (E ∩ F)`. -/ +noncomputable def rankCost (E F : Submodule K V) : ℤ := + (Module.finrank K E : ℤ) + Module.finrank K F - 2 * Module.finrank K (E ⊓ F : Submodule K V) + +/-- H2: the paid rank is at least the dimension change. -/ +theorem rankCost_ge_abs [FiniteDimensional K V] (E F : Submodule K V) : + |(Module.finrank K F : ℤ) - Module.finrank K E| ≤ rankCost E F := by + have h1 : Module.finrank K (E ⊓ F : Submodule K V) ≤ Module.finrank K E := + Submodule.finrank_mono inf_le_left + have h2 : Module.finrank K (E ⊓ F : Submodule K V) ≤ Module.finrank K F := + Submodule.finrank_mono inf_le_right + unfold rankCost + rw [abs_le]; constructor <;> omega + +/-- Nested frames pay exactly the dimension gap. -/ +theorem rankCost_nested {E F : Submodule K V} (h : E ≤ F) : + rankCost E F = (Module.finrank K F : ℤ) - Module.finrank K E := by + unfold rankCost; rw [inf_eq_left.mpr h]; ring + +/-- Parity: the paid rank has the parity of the dimension change. -/ +theorem rankCost_parity (E F : Submodule K V) : + Even (rankCost E F - ((Module.finrank K F : ℤ) - Module.finrank K E)) := by + unfold rankCost + exact ⟨(Module.finrank K E : ℤ) - Module.finrank K (E ⊓ F : Submodule K V), by ring⟩ + +end Rank + +/-! ## §3 Field paths, telescoping, Theorem C and `Λ_f ≥ 0` -/ + +/-- An abstract field history: `dim j` is the frame dimension after `j` events and `cost j` the +rank paid at event `j` (zero for warps and scalar operations). Hypothesis `hcost` is H1+H2: +free events preserve dimension, paid ones cost at least the dimension change. -/ +structure FieldPath where + n : ℕ + dim : ℕ → ℤ + cost : ℕ → ℤ + hcost : ∀ j ∈ range n, |dim (j + 1) - dim j| ≤ cost j + +namespace FieldPath + +variable (P : FieldPath) + +/-- Credited rank `R_f = dim final - dim start` (P:19 / H3). -/ +def R : ℤ := P.dim P.n - P.dim 0 +/-- Paid mass. -/ +def mass : ℤ := ∑ j ∈ range P.n, P.cost j +/-- Down mass: total size of descents. -/ +def down : ℤ := ∑ j ∈ range P.n, max (-(P.dim (j + 1) - P.dim j)) 0 + +theorem cost_nonneg {j : ℕ} (hj : j ∈ range P.n) : 0 ≤ P.cost j := + (abs_nonneg _).trans (P.hcost j hj) + +theorem abs_split (x : ℤ) : |x| = x + 2 * max (-x) 0 := by + rcases abs_cases x with ⟨h1, h2⟩ | ⟨h1, h2⟩ <;> + rcases max_cases (-x) 0 with ⟨h3, h4⟩ | ⟨h3, h4⟩ <;> omega + +/-- Telescoping of the dimension changes. -/ +theorem telescope : ∑ j ∈ range P.n, (P.dim (j + 1) - P.dim j) = P.R := + sum_range_sub P.dim P.n + +/-- The integer path identity: `Σ|Δ| = R + 2·down`. -/ +theorem sum_abs_eq : ∑ j ∈ range P.n, |P.dim (j + 1) - P.dim j| = P.R + 2 * P.down := by + simp_rw [abs_split] + rw [sum_add_distrib, ← mul_sum, telescope]; rfl + +theorem down_nonneg : 0 ≤ P.down := sum_nonneg fun _ _ => le_max_right _ _ + +/-- Paid mass is at least `R + 2·down`. -/ +theorem mass_ge : P.R + 2 * P.down ≤ P.mass := by + rw [← sum_abs_eq]; exact sum_le_sum P.hcost + +/-- Theorem C (mass): `Hnet_f = mass - R ≥ 0`. -/ +theorem hnet_nonneg : P.R ≤ P.mass := by linarith [P.mass_ge, P.down_nonneg] + +/-- Theorem C (mass) with inverse credit: crediting every descent as well keeps `Hnet ≥ 0`. -/ +theorem hnet_inverse_nonneg : P.R + P.down ≤ P.mass := by linarith [P.mass_ge, P.down_nonneg] + +/-- Paid `t`-moment of the field. -/ +noncomputable def moment (t : ℝ) : ℝ := ∑ j ∈ range P.n, ((P.cost j : ℝ)) ^ t +/-- Fragmentation loss `Λ_f(t) = Σ_j c_j^t - R_f^t`. -/ +noncomputable def lam (t : ℝ) : ℝ := P.moment t - ((P.R : ℝ)) ^ t + +theorem cast_mass : ((P.mass : ℤ) : ℝ) = ∑ j ∈ range P.n, ((P.cost j : ℝ)) := by + unfold mass; push_cast; rfl + +/-- `(mass)^t ≤ moment`. -/ +theorem mass_rpow_le {t : ℝ} (ht0 : 0 < t) (ht1 : t ≤ 1) : + ((P.mass : ℝ)) ^ t ≤ P.moment t := by + rw [cast_mass] + exact rpow_sum_le _ _ (fun j hj => by exact_mod_cast P.cost_nonneg hj) ht0 ht1 + +/-- Theorem B's inequality: `Λ_f(t) ≥ 0` for `0 < t ≤ 1` whenever `R_f ≥ 0`. -/ +theorem lam_nonneg {t : ℝ} (hR : 0 ≤ P.R) (ht0 : 0 < t) (ht1 : t ≤ 1) : 0 ≤ P.lam t := by + have h1 : ((P.R : ℝ)) ^ t ≤ ((P.mass : ℝ)) ^ t := + Real.rpow_le_rpow (by exact_mod_cast hR) (by exact_mod_cast P.hnet_nonneg) ht0.le + unfold lam; linarith [P.mass_rpow_le ht0 ht1] + +/-- Theorem C (moment): a helper credited `R_f` contributes `R_f^t - moment = -Λ_f ≤ 0`. -/ +theorem helper_contribution_nonpos {t : ℝ} (hR : 0 ≤ P.R) (ht0 : 0 < t) (ht1 : t ≤ 1) : + ((P.R : ℝ)) ^ t - P.moment t ≤ 0 := by + have := P.lam_nonneg hR ht0 ht1; unfold lam at this; linarith + +/-- Strictness: two climbs of positive rank make `Λ_f(t) > 0` for `0 < t < 1`. +So `Λ_f = 0` forces at most one paid job. -/ +theorem lam_pos_of_two {t : ℝ} (hR : 0 ≤ P.R) (ht0 : 0 < t) (ht1 : t < 1) {i k : ℕ} + (hi : i ∈ range P.n) (hk : k ∈ range P.n) (hik : i ≠ k) + (hci : 0 < P.cost i) (hck : 0 < P.cost k) : 0 < P.lam t := by + have h1 : ((P.R : ℝ)) ^ t ≤ ((P.mass : ℝ)) ^ t := + Real.rpow_le_rpow (by exact_mod_cast hR) (by exact_mod_cast P.hnet_nonneg) ht0.le + have h2 : ((P.mass : ℝ)) ^ t < P.moment t := by + rw [cast_mass] + exact rpow_sum_lt _ (fun j => (P.cost j : ℝ)) (fun j hj => by exact_mod_cast P.cost_nonneg hj) + hi hk hik (by exact_mod_cast hci) (by exact_mod_cast hck) ht0 ht1 + unfold lam; linarith + +end FieldPath + +/-! ### Bridge: a frame history of actual subspaces is a `FieldPath` + +Events are either paid transports (cost `rankCost`, H2) or free events (warps, scalar ops) that +preserve the frame dimension (H1). -/ +section Bridge + +variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] + +/-- The `FieldPath` of a frame history `E 0, E 1, …, E n` with paid steps `paid`. -/ +noncomputable def FieldPath.ofSubspaces (n : ℕ) (E : ℕ → Submodule K V) (paid : ℕ → Prop) + [DecidablePred paid] + (hfree : ∀ j ∈ range n, ¬ paid j → + Module.finrank K (E (j + 1)) = Module.finrank K (E j)) : FieldPath where + n := n + dim j := Module.finrank K (E j) + cost j := if paid j then rankCost (E j) (E (j + 1)) else 0 + hcost j hj := by + by_cases h : paid j + · rw [if_pos h]; exact rankCost_ge_abs _ _ + · rw [if_neg h, hfree j hj h]; simp + +/-- Theorem B/C for subspace histories: `Λ_f(t) ≥ 0` whenever the final frame is at least as +large as the start (helpers: strict `S ⊂ T`, P:19; mains: contract endpoints). -/ +theorem lam_nonneg_ofSubspaces (n : ℕ) (E : ℕ → Submodule K V) (paid : ℕ → Prop) + [DecidablePred paid] + (hfree : ∀ j ∈ range n, ¬ paid j → + Module.finrank K (E (j + 1)) = Module.finrank K (E j)) + (hR : Module.finrank K (E 0) ≤ Module.finrank K (E n)) {t : ℝ} (ht0 : 0 < t) (ht1 : t ≤ 1) : + 0 ≤ (FieldPath.ofSubspaces n E paid hfree).lam t := by + apply FieldPath.lam_nonneg _ _ ht0 ht1 + show (0 : ℤ) ≤ (Module.finrank K (E n) : ℤ) - Module.finrank K (E 0) + omega + +end Bridge + +/-! ## §4 Theorem B: the per-call decomposition identity + +Native per-call moment `φ = Σ_helpers h^t - Σ_paid r^t`. Partition paid jobs into helper fields, +main fields and centre jobs. Helpers are credited `h_f = R_f^t`; every main has `R_f = d`. +Then `φ = -(#mains)·d^t - centre - Σ_f Λ_f`. -/ +theorem decomposition {ι κ : Type*} (helpers : Finset ι) (mains : Finset κ) + (credit : ι → ℝ) (paidH : ι → ℝ) (paidM : κ → ℝ) (dt centre : ℝ) : + (∑ i ∈ helpers, credit i) - (∑ i ∈ helpers, paidH i + ∑ k ∈ mains, paidM k + centre) + = -(mains.card : ℝ) * dt - centre + - (∑ i ∈ helpers, (paidH i - credit i) + ∑ k ∈ mains, (paidM k - dt)) := by + simp only [sum_sub_distrib, sum_const, nsmul_eq_mul]; ring + +/-! ## §5 The descent price -/ + +namespace FieldPath + +variable (P : FieldPath) + +/-- Descent price: a field with fixed endpoints (`R ≥ 0`) and one descent of rank `r` at step `k` +pays `Λ_f(t) ≥ r^t + (R+r)^t - R^t`. -/ +theorem descent_price {t : ℝ} (hR : 0 ≤ P.R) (ht0 : 0 < t) (ht1 : t ≤ 1) {k : ℕ} + (hk : k ∈ range P.n) {r : ℤ} (hr : 0 ≤ r) (hdesc : P.dim (k + 1) - P.dim k = -r) : + ((r : ℝ)) ^ t + (((P.R + r : ℤ) : ℝ)) ^ t - ((P.R : ℝ)) ^ t ≤ P.lam t := by + -- the descent step pays at least r + have hck : r ≤ P.cost k := by + have := P.hcost k hk; rw [hdesc, abs_neg, abs_of_nonneg hr] at this; exact this + -- the remaining steps carry up-mass at least R + r + have hrest : P.R + r ≤ ∑ j ∈ (range P.n).erase k, P.cost j := by + have htel := P.telescope + rw [← add_sum_erase _ _ hk, hdesc] at htel + have : ∑ j ∈ (range P.n).erase k, (P.dim (j + 1) - P.dim j) + ≤ ∑ j ∈ (range P.n).erase k, P.cost j := + sum_le_sum fun j hj => (le_abs_self _).trans (P.hcost j (mem_of_mem_erase hj)) + linarith + have hnn : ∀ j ∈ (range P.n).erase k, (0 : ℝ) ≤ (P.cost j : ℝ) := + fun j hj => by exact_mod_cast P.cost_nonneg (mem_of_mem_erase hj) + have e1 : ((r : ℝ)) ^ t ≤ ((P.cost k : ℝ)) ^ t := + Real.rpow_le_rpow (by exact_mod_cast hr) (by exact_mod_cast hck) ht0.le + have e2 : (((P.R + r : ℤ) : ℝ)) ^ t ≤ (∑ j ∈ (range P.n).erase k, (P.cost j : ℝ)) ^ t := by + apply Real.rpow_le_rpow (by exact_mod_cast (by linarith : (0 : ℤ) ≤ P.R + r)) + · exact_mod_cast hrest + · exact ht0.le + have e3 := rpow_sum_le ((range P.n).erase k) (fun j => (P.cost j : ℝ)) hnn ht0 ht1 + have hm : P.moment t = ((P.cost k : ℝ)) ^ t + + ∑ j ∈ (range P.n).erase k, ((P.cost j : ℝ)) ^ t := by + unfold moment; rw [← add_sum_erase _ _ hk] + unfold lam; rw [hm]; linarith + +/-- Descent price, worst case over `R ≤ 9` (frames live in `F₂⁹`): +`Λ_f(t) ≥ r^t + (9+r)^t - 9^t`. -/ +theorem descent_price_nine {t : ℝ} (hR : 0 ≤ P.R) (hR9 : P.R ≤ 9) (ht0 : 0 < t) (ht1 : t ≤ 1) + {k : ℕ} (hk : k ∈ range P.n) {r : ℤ} (hr : 0 ≤ r) (hdesc : P.dim (k + 1) - P.dim k = -r) : + ((r : ℝ)) ^ t + ((9 : ℝ) + r) ^ t - (9 : ℝ) ^ t ≤ P.lam t := by + have h := P.descent_price hR ht0 ht1 hk hr hdesc + have hm := rpow_increment_antitone (x := (P.R : ℝ)) (y := 9) (r := (r : ℝ)) + (by exact_mod_cast hR) (by exact_mod_cast hR9) (by exact_mod_cast hr) ht0.le ht1 + push_cast at h + linarith + +end FieldPath + +/-! ## §6 A30-CUT: level crossings and the dual certificate `y = 8^t / 8` -/ + +section Levels + +/-- Step `a → b` crosses level `λ` (upward or downward). -/ +def Crosses (a b l : ℤ) : Prop := (a < l ∧ l ≤ b) ∨ (b < l ∧ l ≤ a) + +instance (a b l : ℤ) : Decidable (Crosses a b l) := by unfold Crosses; infer_instance + +/-- A step crosses at most `|b - a|` levels of any level set (rank is 1-Lipschitz). -/ +theorem levels_crossed_le (L : Finset ℤ) (a b : ℤ) : + ((L.filter (Crosses a b)).card : ℤ) ≤ |b - a| := by + have hsub : L.filter (Crosses a b) ⊆ Ioc (min a b) (max a b) := by + intro l hl + rw [mem_filter] at hl + rw [mem_Ioc] + rcases hl.2 with ⟨h1, h2⟩ | ⟨h1, h2⟩ + · exact ⟨lt_of_le_of_lt (min_le_left _ _) h1, le_trans h2 (le_max_right _ _)⟩ + · exact ⟨lt_of_le_of_lt (min_le_right _ _) h1, le_trans h2 (le_max_left _ _)⟩ + have hc := card_le_card hsub + rw [Int.card_Ioc] at hc + have : ((max a b - min a b).toNat : ℤ) = |b - a| := by + rw [Int.toNat_of_nonneg (by linarith [min_le_max (a := a) (b := b)])] + rcases le_total a b with h | h + · rw [max_eq_right h, min_eq_left h, abs_of_nonneg (by linarith)] + · rw [max_eq_left h, min_eq_right h, abs_of_nonpos (by linarith)]; ring + omega + +/-- Per-level telescoping: at every step, (up-crossing) − (down-crossing) at level `λ` equals the +change of the indicator `[λ ≤ dim]`. -/ +theorem step_level (a b l : ℤ) : + ((if a < l ∧ l ≤ b then 1 else 0) - (if b < l ∧ l ≤ a then 1 else 0) : ℤ) + = (if l ≤ b then 1 else 0) - (if l ≤ a then 1 else 0) := by + split_ifs <;> omega + +namespace FieldPath + +variable (P : FieldPath) + +/-- Up-crossings of level `λ` along the path. -/ +def up (l : ℤ) : ℤ := ∑ j ∈ range P.n, if P.dim j < l ∧ l ≤ P.dim (j + 1) then 1 else 0 +/-- Down-crossings of level `λ` along the path. -/ +def dn (l : ℤ) : ℤ := ∑ j ∈ range P.n, if P.dim (j + 1) < l ∧ l ≤ P.dim j then 1 else 0 + +/-- Per-level telescoping: `up λ - down λ = [λ ≤ final] - [λ ≤ start]`. -/ +theorem up_sub_dn (l : ℤ) : + P.up l - P.dn l = (if l ≤ P.dim P.n then 1 else 0) - (if l ≤ P.dim 0 then 1 else 0) := by + unfold up dn + rw [← sum_sub_distrib] + simp_rw [step_level] + exact sum_range_sub (fun j => if l ≤ P.dim j then (1 : ℤ) else 0) P.n + +/-- Each job's rank pays for every level it crosses: `Σ_{λ∈L} (up λ + down λ) ≤ mass`. -/ +theorem crossings_le_mass (L : Finset ℤ) : ∑ l ∈ L, (P.up l + P.dn l) ≤ P.mass := by + unfold up dn mass + simp_rw [← sum_add_distrib] + rw [sum_comm] + refine sum_le_sum fun j hj => ?_ + have h1 : ∑ l ∈ L, ((if P.dim j < l ∧ l ≤ P.dim (j + 1) then (1 : ℤ) else 0) + + (if P.dim (j + 1) < l ∧ l ≤ P.dim j then 1 else 0)) + = ((L.filter (Crosses (P.dim j) (P.dim (j + 1)))).card : ℤ) := by + rw [card_filter]; push_cast + refine sum_congr rfl fun l _ => ?_ + unfold Crosses; split_ifs <;> omega + rw [h1] + exact (levels_crossed_le L _ _).trans (P.hcost j hj) + +end FieldPath + +end Levels + +section Dual + +variable {t : ℝ} + +/-- `y = 8^t/8 < 1` for `t < 1`. -/ +theorem y_lt_one (ht1 : t < 1) : (8 : ℝ) ^ t / 8 < 1 := by + have : (8 : ℝ) ^ t < (8 : ℝ) ^ (1 : ℝ) := Real.rpow_lt_rpow_of_exponent_lt (by norm_num) ht1 + rw [Real.rpow_one] at this; rw [div_lt_one (by norm_num)]; exact this + +/-- Dual feasibility for an owned job of rank `a`: `a^t ≥ y · min(a, 8)` with `y = 8^t/8`. -/ +theorem owned_dual {a : ℝ} (ha : 0 ≤ a) (ht0 : 0 < t) (ht1 : t ≤ 1) : + (8 : ℝ) ^ t / 8 * min a 8 ≤ a ^ t := by + rcases le_total a 8 with h | h + · rw [min_eq_left h] + have := mul_rpow_sub_one_le ha h ht1 ht0 (t := t) + rw [Real.rpow_sub_one (by norm_num : (8 : ℝ) ≠ 0)] at this + linarith [show (8 : ℝ) ^ t / 8 * a = a * ((8 : ℝ) ^ t / 8) by ring] + · rw [min_eq_right h] + have := Real.rpow_le_rpow (by norm_num : (0 : ℝ) ≤ 8) h ht0.le + linarith + +/-- Dual feasibility, credited field with `k = 1`: two or more jobs of rank `≥ 1` with total +`≥ R + 2` pay `Σ c^t ≥ R^t + 1`, so the loss `≥ 1 > y`. -/ +theorem credited_k1 {ι : Type*} [DecidableEq ι] (s : Finset ι) (c : ι → ℝ) + (hc : ∀ j ∈ s, 1 ≤ c j) {i k : ι} (hi : i ∈ s) (hk : k ∈ s) (hik : i ≠ k) + {R : ℝ} (hR : 0 ≤ R) (hsum : R + 2 ≤ ∑ j ∈ s, c j) (ht0 : 0 < t) (ht1 : t ≤ 1) : + R ^ t + 1 ≤ ∑ j ∈ s, c j ^ t := by + have hk' : k ∈ s.erase i := mem_erase.mpr ⟨hik.symm, hk⟩ + have hce : ∀ j ∈ s.erase i, 0 ≤ c j := fun j hj => by linarith [hc j (mem_of_mem_erase hj)] + set B := ∑ j ∈ s.erase i, c j with hBdef + have hB1 : 1 ≤ B := le_trans (hc k hk) (single_le_sum hce hk') + have hci := hc i hi + have hsplit : ∑ j ∈ s, c j = c i + B := (add_sum_erase s c hi).symm + have hsplit' : ∑ j ∈ s, c j ^ t = c i ^ t + ∑ j ∈ s.erase i, c j ^ t := + (add_sum_erase s (fun j => c j ^ t) hi).symm + have hBt := rpow_sum_le (s.erase i) c hce ht0 ht1 + -- exchange: c_i^t + B^t ≥ 1^t + (c_i + B - 1)^t + have hx := rpow_increment_antitone (x := 1) (y := B) (r := c i - 1) (by norm_num) hB1 + (by linarith) ht0.le ht1 + have e1 : B + (c i - 1) = c i + B - 1 := by ring + have e2 : (1 : ℝ) + (c i - 1) = c i := by ring + rw [e1, e2, Real.one_rpow] at hx + have hmono : R ^ t ≤ (c i + B - 1) ^ t := + Real.rpow_le_rpow hR (by linarith) ht0.le + rw [hsplit']; linarith + +/-- Bernoulli-type bound used for the numerics: `9^(t-1) ≥ 25/27` for `t ≥ 99/100`. -/ +theorem nine_rpow_sub_one_ge (ht : 99 / 100 ≤ t) (ht1 : t ≤ 1) : + (25 / 27 : ℝ) ≤ (9 : ℝ) ^ (t - 1) := by + have hb := rpow_one_add_le_one_add_mul_self (s := 8) (by norm_num) (p := 1 - t) + (by linarith) (by linarith) + have hpos : 0 < (9 : ℝ) ^ (1 - t) := Real.rpow_pos_of_pos (by norm_num) _ + have hle : (9 : ℝ) ^ (1 - t) ≤ 27 / 25 := by norm_num at hb ⊢; linarith + have : (9 : ℝ) ^ (t - 1) = ((9 : ℝ) ^ (1 - t))⁻¹ := by + rw [← Real.rpow_neg (by norm_num)]; ring_nf + rw [this, le_inv_comm₀ (by norm_num) hpos] + linarith [show ((25 / 27 : ℝ))⁻¹ = 27 / 25 by norm_num] + +/-- `x^t ≤ x + 1` for `x ≥ 0`, `0 ≤ t ≤ 1`. -/ +theorem rpow_le_add_one {x : ℝ} (hx : 0 ≤ x) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : x ^ t ≤ x + 1 := by + rcases le_total x 1 with h | h + · linarith [Real.rpow_le_one hx h ht0] + · have := Real.rpow_le_rpow_of_exponent_le h ht1 + rw [Real.rpow_one] at this; linarith + +/-- Dual feasibility, credited field with `k ≥ 2` (for `t ∈ [0.99, 1]`): jobs of rank `≤ 9` +with total `≥ R + 2k`, `0 ≤ R ≤ 9`, have loss `Σ c^t - R^t ≥ y·k`. -/ +theorem credited_k2 {ι : Type*} (s : Finset ι) (c : ι → ℝ) (hc0 : ∀ j ∈ s, 0 ≤ c j) + (hc9 : ∀ j ∈ s, c j ≤ 9) {R k : ℝ} (hR : 0 ≤ R) (hR9 : R ≤ 9) (hk : 2 ≤ k) + (hsum : R + 2 * k ≤ ∑ j ∈ s, c j) (ht : 99 / 100 ≤ t) (ht1 : t ≤ 1) : + (8 : ℝ) ^ t / 8 * k ≤ ∑ j ∈ s, c j ^ t - R ^ t := by + have ht0 : 0 < t := by linarith + set q := (9 : ℝ) ^ (t - 1) with hq + have hq0 : 25 / 27 ≤ q := nine_rpow_sub_one_ge ht ht1 + have hchord : ∑ j ∈ s, c j * q ≤ ∑ j ∈ s, c j ^ t := + sum_le_sum fun j hj => mul_rpow_sub_one_le (hc0 j hj) (hc9 j hj) ht1 ht0 + rw [← sum_mul] at hchord + have hy : (8 : ℝ) ^ t / 8 ≤ 1 := by + rcases ht1.eq_or_lt with h | h + · rw [h, Real.rpow_one]; norm_num + · exact (y_lt_one h).le + have hRt := rpow_le_add_one hR ht0.le ht1 + have hy0 : 0 ≤ (8 : ℝ) ^ t / 8 := by positivity + nlinarith [mul_le_mul_of_nonneg_left hy (by linarith : (0 : ℝ) ≤ k), + mul_le_mul_of_nonneg_right hsum (by linarith : (0 : ℝ) ≤ q), + mul_le_mul_of_nonneg_left hq0 (by linarith : (0 : ℝ) ≤ R + 2 * k)] + +end Dual + +end Skel + +#print axioms Skel.rpow_sum_le +#print axioms Skel.rpow_sum_lt +#print axioms Skel.rpow_increment_antitone +#print axioms Skel.rankCost_ge_abs +#print axioms Skel.rankCost_nested +#print axioms Skel.rankCost_parity +#print axioms Skel.FieldPath.sum_abs_eq +#print axioms Skel.FieldPath.hnet_nonneg +#print axioms Skel.FieldPath.hnet_inverse_nonneg +#print axioms Skel.FieldPath.lam_nonneg +#print axioms Skel.FieldPath.helper_contribution_nonpos +#print axioms Skel.FieldPath.lam_pos_of_two +#print axioms Skel.lam_nonneg_ofSubspaces +#print axioms Skel.decomposition +#print axioms Skel.FieldPath.descent_price +#print axioms Skel.FieldPath.descent_price_nine +#print axioms Skel.levels_crossed_le +#print axioms Skel.FieldPath.up_sub_dn +#print axioms Skel.FieldPath.crossings_le_mass +#print axioms Skel.owned_dual +#print axioms Skel.credited_k1 +#print axioms Skel.credited_k2 diff --git a/research/fragmentation-ceiling/lean/lake-manifest.json b/research/fragmentation-ceiling/lean/lake-manifest.json new file mode 100644 index 0000000000..818d5c2270 --- /dev/null +++ b/research/fragmentation-ceiling/lean/lake-manifest.json @@ -0,0 +1,117 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "55b7917b472489c7c56a0fa6393af05cfd536599", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "55b7917b472489c7c56a0fa6393af05cfd536599", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "57d3325be72a842920813bcb40f96a6f7393c185", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0-rc1", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "Skel", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/research/fragmentation-ceiling/lean/lakefile.toml b/research/fragmentation-ceiling/lean/lakefile.toml new file mode 100644 index 0000000000..75221c4280 --- /dev/null +++ b/research/fragmentation-ceiling/lean/lakefile.toml @@ -0,0 +1,10 @@ +name = "Skel" +defaultTargets = ["Skel"] + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "55b7917b472489c7c56a0fa6393af05cfd536599" + +[[lean_lib]] +name = "Skel" diff --git a/research/fragmentation-ceiling/lean/lean-toolchain b/research/fragmentation-ceiling/lean/lean-toolchain new file mode 100644 index 0000000000..fd85b262bf --- /dev/null +++ b/research/fragmentation-ceiling/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.0-rc1 diff --git a/research/fragmentation-ceiling/verify.py b/research/fragmentation-ceiling/verify.py new file mode 100644 index 0000000000..4a676e0397 --- /dev/null +++ b/research/fragmentation-ceiling/verify.py @@ -0,0 +1,205 @@ +#!/usr/bin/env python3 +"""Rebuild the fragmentation loss Lambda of the public #4610 word and the exact ship threshold. + +Python standard library only (decimal, 60 digits); about 6 s. Reads the public #4610 package +(Cao Yifan / intqwq), nothing else: + research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz + research/kappa-round3-warp-20261022/ARITHMETIC.json + research/kappa-round3-warp-lean-20261022/NumericalMoments.lean + +Usage: python3 -B verify.py [PKG_ROOT] [BAR] + PKG_ROOT directory that contains research/kappa-round3-warp-20261022 (default: searched upward + from this file, then $INTMULT_PKG). + BAR internal bar, default 0.0030233; t* = 1 - BAR. +Exit status 0 iff every assertion passes. Output lines are numbered [k]; PROOF.md cites them. +""" +import sys, os, json, gzip, re, collections +from decimal import Decimal as D, getcontext +getcontext().prec = 60 + +def find_pkg(): + if len(sys.argv) > 1: return sys.argv[1] + if os.environ.get('INTMULT_PKG'): return os.environ['INTMULT_PKG'] + here = os.path.dirname(os.path.abspath(__file__)) + p = here + for _ in range(6): + for cand in (p, os.path.join(p, 'wt')): + if os.path.isdir(os.path.join(cand, 'research', 'kappa-round3-warp-20261022')): return cand + p = os.path.dirname(p) + sys.exit('cannot find the #4610 package; pass PKG_ROOT') +PKG = find_pkg() +BAR = D(sys.argv[2]) if len(sys.argv) > 2 else D('0.0030233') +TS = 1 - BAR +W3 = PKG + '/research/kappa-round3-warp-20261022/' +LN = PKG + '/research/kappa-round3-warp-lean-20261022/NumericalMoments.lean' +v, d = 112, 8 + +def pw(x, t): + x = D(x) + return D(0) if x == 0 else (t * x.ln()).exp() +def mom(Dct, t): return sum(D(n) * pw(r, t) for r, n in Dct.items()) +def fmt(x, k=10): return f'{x:.{k}f}' +def near(x, ref, tol='1e-9'): return abs(D(x) - D(ref)) < D(tol) +default_bar = (BAR == D('0.0030233')) + +# [1] public profiles and the controller family +A = json.load(open(W3 + 'ARITHMETIC.json')) +H = {int(k): n for k, n in A['local_helpers'].items()} +N = {int(k): n for k, n in A['local_paid'].items()} +lean = open(LN).read() +def lean_poly(name): + body = re.search(r'def ' + name + r' \(t : ℝ\) : ℝ :=(.*?)\n\n', lean, re.S).group(1) + return {int(r): int(n) for n, r in re.findall(r'(\d+) \* \((\d+) : ℝ\) \^ t', body)} +T_pub, P_pub = lean_poly('targetMoment'), lean_poly('paidMoment') + +def inv(p, a, H, N, ports=v, block=d): + T = collections.Counter({r: (p + 2) * n for r, n in H.items()}) + P = collections.Counter({r: (p + 2) * n for r, n in N.items()}) + P[1] += ports * (p - 1); T[1 + block * (p + 2)] += 2 * ports + for L in (a, p - 1 - a): + for j in range(1, L + 1): + T[1 + block * (j + 1)] += 2 * ports; P[block * (j + 1)] += 2 * ports + return dict(T), dict(P) +T16, P16 = inv(16, 7, H, N) +assert T16 == T_pub and P16 == P_pub, 'controller formula does not match the public invoice' +print('[1] kap-family formula at p16 a7 reproduces the public Lean invoice exactly:', + len(T_pub), 'target and', len(P_pub), 'paid coefficients') + +# [2] per-field climbs from the public word, both orientations +w = json.loads(gzip.decompress(open(W3 + 'ACTUAL-WORD.json.gz', 'rb').read())) +c = w['canonical']; fr = c['frames']; nf = len(c['start']) +R = [len(fr[c['final'][f]]) - len(fr[c['start'][f]]) for f in range(nf)] +res = {} +for orient in ('forward', 'backward'): + jobs = collections.defaultdict(list); cur = list(c['start']); ncen = 0 + for e in w['programs'][orient]: + if e[0] == 'climb': + f, a_, b_, r = e[2], e[3], e[4], e[5] + assert cur[f] == a_ and r == len(fr[b_]) - len(fr[a_]) and r > 0, e # H1/H2: nested ascending climb + jobs[f].append(r); cur[f] = b_ + elif e[0] == 'warp': + f, a_, b_ = e[1][1], e[3], e[4] + assert cur[f] == a_ and len(fr[a_]) == len(fr[b_]), e # H1: warps preserve dimension + cur[f] = b_ + elif e[0] == 'center': + ncen += 1 + assert cur == list(c['final']) + assert all(sum(jobs[f]) == R[f] for f in range(nf)) # telescoping + prof = collections.Counter(r for f in range(nf) for r in jobs[f]); prof[8] += 8 + assert dict(prof) == N, (orient, dict(prof), N) + res[orient] = jobs + print(f'[2] {orient}: {nf} fields replay start->final; all climbs nested, rank = dim gap; sum climbs = R_f on all fields; ' + f'climb profile + 8 centre jobs = ARITHMETIC local_paid; centre events {ncen}') +nh = sum(H.values()); nm = nf - nh +assert all(R[f] == d for f in range(nm)) and collections.Counter(R[nm:]) == collections.Counter(H) +print(f'[3] mains: {nm} fields with R_f = {d}; helpers: {nh} fields with R_f census = local_helpers {H}') + +def Lam(jobs, t, fields): + return sum(sum(pw(x, t) for x in jobs[f]) - pw(R[f], t) for f in fields) +lams = {} +for orient in ('forward', 'backward'): + jobs = res[orient] + Lh, Lm = Lam(jobs, TS, range(nm, nf)), Lam(jobs, TS, range(nm)) + lams[orient] = Lh + Lm + print(f'[4] {orient}: Lambda(t*) = {fmt(Lh + Lm)} (helpers {fmt(Lh)}, mains {fmt(Lm)})') +assert lams['forward'] == lams['backward'] +jobs = res['forward']; L = lams['forward'] + +# [5] Theorem B identity +phi = mom(H, TS) - mom(N, TS) +centre = 8 * pw(8, TS) +resid = phi + 2 * v * pw(d, TS) + centre + L +print(f'[5] phi(t*) = {fmt(phi)}; -2v d^t* - 8*8^t* - Lambda = {fmt(-2*v*pw(d, TS) - centre - L)}; residual {resid:.2E}') +assert abs(resid) < D('1e-50') + +# [6] ship threshold +Gam = lambda p, a, t: (lambda TP: mom(TP[0], t) - mom(TP[1], t))(inv(p, a, {}, {})) +G16 = Gam(16, 7, TS); phistar16 = -G16 / 18 +Lstar = -phistar16 - (2 * v + 8) * pw(d, TS) +f_ts = mom(T_pub, TS) - mom(P_pub, TS) +print(f'[6] p16 a7: phi* = -Gamma(t*)/18 = {fmt(phistar16)}; Lambda* = -phi* - 232*8^t* = {fmt(Lstar)}') +print(f' Lambda(#4610) - Lambda* = {fmt(L - Lstar)} per call; 18*(Lambda*-Lambda) = {fmt(18*(Lstar - L))}; public invoice f(t*) = {fmt(f_ts)}') +assert abs(18 * (Lstar - L) - f_ts) < D('1e-40') + +# [7] Corollary A1: p16 is the best controller of the kap family at t* +best = max((Gam(p, a, TS) / (p + 2), p, a) for p in range(3, 61) for a in range(p)) +okA1 = best[1] == 16 and best[2] in (7, 8) and abs(best[0] + phistar16) < D('1e-45') +print(f'[7] max over kap family p=3..60, all a: Gamma/(p+2) best at p={best[1]} a={best[2]} (phi* = {fmt(-best[0])}); ' + f'p16 a7 is the max (a and p-1-a give the same invoice): {okA1}') +assert okA1 +# [7b] the rest of the family: exact max for p = 1..PMAX via prefix sums, and for p > PMAX the bound +# Gamma/(p+2) <= F(PMAX+1) + 2v*delta_1 - v, with F(p) = 2v(1+8(p+2))^t/(p+2) decreasing in p and +# delta_j = (1+8(j+1))^t - (8(j+1))^t <= delta_1 (Lemma 3), each bracket term 2v*delta_j - v > 0. +PMAX = 400 +dl = [D(0)] + [pw(1 + d * (j + 1), TS) - pw(d * (j + 1), TS) for j in range(1, PMAX + 1)] +S = [D(0)] +for j in range(1, PMAX + 1): S.append(S[-1] + dl[j]) +Fp = lambda p: 2 * v * pw(1 + d * (p + 2), TS) / (p + 2) +best_all = max((F + (2 * v * (S[a] + S[p - 1 - a]) - v * (p - 1)) / (p + 2), p, a) + for p, F in ((p, Fp(p)) for p in range(1, PMAX + 1)) for a in range(p)) +tail = Fp(PMAX + 1) + 2 * v * dl[1] - v +okA1b = best_all[1] == 16 and abs(best_all[0] + phistar16) < D('1e-45') and tail < -phistar16 and all(2 * v * x > v for x in dl[1:]) +print(f'[7b] exact max over p=1..{PMAX}: p={best_all[1]} a={best_all[2]}; tail bound for p>{PMAX}: {fmt(tail, 4)} < {fmt(-phistar16, 4)}: {okA1b}') +assert okA1b + +# [8] root of the public invoice +def froot(T, P): + lo, hi = D('1e-6'), D('0.05') + for _ in range(140): + m = (lo + hi) / 2 + if mom(T, 1 - m) - mom(P, 1 - m) > 0: lo = m + else: hi = m + return lo +kap = froot(T_pub, P_pub) +print(f'[8] public invoice root kappa = {kap:.13f} (package: in (0.0030217758, 0.0030217759))') +assert D('0.0030217758') < kap < D('0.0030217759') +print('SHIP TEST: a word in this family clears the bar iff Lambda(t*) <=', fmt(Lstar, 7), '; #4610 has', fmt(L, 7)) + +# [9] descent price (Theorem D), merge values +price = lambda r: pw(r, TS) + pw(9 + r, TS) - pw(9, TS) +n_desc = int(Lstar / price(1)) +print('[9] descent price lower bound r^t+(9+r)^t-9^t:', ', '.join(f'r={r}: {fmt(price(r), 5)}' for r in (1, 2, 3, 4)), + f'; max rank-1 descents with Lambda <= Lambda*: {n_desc}') +print('[10] merge values: 1+1->2', fmt(2 - pw(2, TS), 7), ' 4+4->3+5', fmt(2*pw(4, TS) - pw(3, TS) - pw(5, TS), 8), + ' needed per call', fmt(L - Lstar, 7)) + +# [11] A30-CUT dual constants +Lf_max = max(sum(pw(x, TS) for x in jobs[f]) - pw(R[f], TS) for f in range(nf)) +y = pw(8, TS) / 8 +print('[11] A30 dual: y = 8^t/8 =', fmt(y, 6), ' 9^(t-1) =', fmt(pw(9, TS) / 9, 6), ' max_f Lambda_f =', fmt(Lf_max, 5)) +assert y < 1 and pw(9, TS) / 9 >= D(25) / 27 and Lf_max < D('0.06') + +# [12] consistency at #4610's own root: Lambda*(bar = kappa) equals Lambda(t0) +t0 = 1 - kap +Ls0 = -(-(Gam(16, 7, t0) / 18)) - (2 * v + 8) * pw(d, t0) +L0 = Lam(jobs, t0, range(nf)) +print(f'[12] at its own root t0 = 1 - kappa: Lambda(t0) = {fmt(L0)}, Lambda*(bar=kappa) = {fmt(Ls0)}, difference {abs(L0 - Ls0):.2E}') +assert abs(L0 - Ls0) < D('1e-9') + +# [13] budget arithmetic for the centre-free (coded) family: the centre is deleted, nothing else changes +f8 = pw(8, TS) +phi_coded = phi + 8 * f8 +B = phi_coded - phistar16 +print(f'[13] centre-free budget B = phi_coded - phi* = {fmt(B, 12)} per call = 8 f(8) - gap = {fmt(8*f8 - (L - Lstar), 12)}; 8 f(8) = {fmt(8*f8, 10)}') +print(f' whole invoice 18B = {fmt(18*B, 8)}; 144 f(8) = {fmt(144*f8, 8)}; shortfall 144 f(8) - 18B = {fmt(144*f8 - 18*B, 10)} = 18 x gap') +print(f' per negative bank if the positive half is free: 18B/16 = {fmt(18*B/16, 10)}; 53 debt classes x 8 f(8) = {fmt(53*8*f8, 2)}; ' + f'16 banks x 112 f(2) = {fmt(16*112*pw(2, TS), 1)}') +assert abs(B - (8 * f8 - (L - Lstar))) < D('1e-40') +assert 144 * f8 - 18 * B == 18 * (L - Lstar) or abs(144 * f8 - 18 * B - 18 * (L - Lstar)) < D('1e-40') +if default_bar: + assert near(B, '63.577975271157', '1e-9') and near(Lstar, '23.8536932758', '1e-9') and near(L, '23.8746264727', '1e-9') + assert near(L - Lstar, '0.0209331969', '1e-9') and n_desc == 11 + assert near(price(1), '1.99022', '1e-5') and near(price(2), '3.97594', '1e-5') + assert near(53 * 8 * f8, '3370.74', '1e-2') and near(18 * B / 16, '71.5252221801', '1e-9') + +# [14] Lean file hygiene (text-level only; the Lean build is separate, see README) +lp = os.path.join(os.path.dirname(os.path.abspath(__file__)), 'lean', 'Skel.lean') +if os.path.exists(lp): + src = open(lp, encoding='utf-8').read() + code = re.sub(r'/-.*?-/', '', src, flags=re.S) + decls = re.findall(r'^\s*(?:private\s+)?(?:theorem|lemma)\s+(\S+)', code, re.M) + has_sorry = 'sorry' in code + has_axiom = bool(re.search(r'^\s*axiom\b', code, re.M)) + print(f'[14] lean/Skel.lean: {len(decls)} theorem/lemma declarations; "sorry" present: {has_sorry}; "axiom" present: {has_axiom}') + assert 'sorry' not in code +print('ALL CHECKS PASSED')