Replace the TODO(lean-port) sorry with a complete proof of the
projectionOrdering theorem: for positive SourceValue pairs s1 < s2
with s2 ≤ maxExpected, projectToCoding preserves strict ordering
of the Q0_64 values.
The proof uses Nat-only arithmetic (no Float) and handles two cases:
- a2 < d: both values fit in Q0_64 range, ordering follows from
monotonicity of integer division
- a2 = d: a2*s/d = s clamped to q0_64MaxRaw; a1*s/d < q0_64MaxRaw
via the key inequality (d-1)*s < (s-1)*d
Build: 8598 jobs, 0 errors (lake build)
Key change: goormaghtigh_finite_search is no longer an axiom. Replaced
with native_decide proof using nested ∀ x ∈ Icc, ∀ m ∈ Icc, ... which
is fast (avoids constructing a 958K-element Finset).
Also added:
- repunit_mod_pred lemma: R(x,m) ≡ m (mod x-1)
- goormaghtigh_collision_mod lemma: cross-residue sieve
- Theorem now includes 4 ordered forms (adding (2,5,5,3) and
(2,13,90,3) for completeness)
Only goormaghtigh_boundedness remains as axiom.
Build: 8317 jobs, 0 errors.
repunit_collisions_unique proven via native_decide on a 979-element Finset:
only 2 repunit values (31 and 8191) have multiplicity > 1 in [2,90]×[3,13].
goormaghtigh_finite_search remains an axiom (the full finite search
conclusion requires the specific collision pairs, not just their count).
Build: 8317 jobs, 0 errors.
Theorem: For x>1, y>1, m>2, n>2, (x,m)≠(y,n),
if R(x,m) = R(y,n) then (x,m,y,n) = (5,3,2,5) or (90,3,2,13).
Two axioms remain:
- goormaghtigh_finite_search: 979 repunit pairs enumerated in Python,
only 2 collisions (31 and 8191) — verified externally
- goormaghtigh_boundedness: the 16D→0D projection bounds x,y≤90, m,n≤13
(equivalent to the full conjecture — this is the open number theory)
Goormaghtigh's requirement m,n>2 ensures no trivial solutions like
R(6,2)=7=R(2,3). The (x,m)≠(y,n) condition excludes identity solutions.
Build: 8317 jobs, 0 errors.
AGENTS.md: added SpherionTwinPrime architecture section, updated Burgers energy dissipation to parametric form.
spherion_twin_prime.py (20KB): priority-queue walk with polarity energy tuning.
Build: 8598 jobs, 0 errors.
General theorem: for speeds [1,2,...,k] at t = 1/(k+1), the origin
is uncovered. Proves the Lonely Runner Conjecture for the infinite
family of consecutive integer speeds. Subsumes k=2 and k=3 lemmas.
A. ode_existence (AVMRTheorems.lean) — proven via
ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt.
vectorFieldℝ is affine linear (ContDiff ℝ 1 via fun_prop), satisfying
Picard-Lindelöf. Zero sorries remaining in file.
B. BurgersNKConsistency.lean (167 lines) — 4 theorems mapping Burgers
theorems to NK-Hodge-FAMM conditions. Main theorem: energy bounded
for all n via applyViscosity_energy_le induction.
C. LonelyRunner.lean (311 lines) — 10 sections: circle distance, runner
positions, coverage density, scar region, scar complex, beta0.
Proved lonely_k2_speeds_1_2 and lonely_k3_speeds_1_2_3.
Betti bridge to NK-Hodge-FAMM framework.
All builds: 8598/8313 jobs, 0 errors.
- e8_singer_improvement: proven via Singer set as direct witness; (119/120)^k ≤ 1 by
pow_le_one₀, bound follows from mul_le_of_le_one_right.
- erdos30_e8_conditional: proven via interval_sidon_exists (Singer's theorem bridge);
C=1/4, Nat.sqrt ↔ Real.sqrt bridge via nlinarith on squared terms.
- sidon_weight_bound: restated — LHS corrected from σ₃(a+b) sums to σ₃(a)·σ₃(b)
products over unordered pairs (original was INVALID_STATEMENT; E₈ convolution
identity delivers products, not values at pair-sums). Remains ANALYTIC_OPEN.
- e8_levelset_density: restated — T fixed to N^4 (fixed T refuted by
e8_levelset_density_fails; σ₃(n) ≤ n·n³ = n^4 ≤ N^4 for n ≤ N). Fixed base
typo Nat.log N → Nat.log 2 N. Remains ANALYTIC_OPEN sorry.
- §14 summary updated with proven theorems and restatement notes.
- Add merkle_tensegrity_load_equation_generator.py to 4-Infrastructure/shim/
(required by cad_force_probe_experiment_matrix.py import).
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The existence half of Picard-Lindelöf for finite-dimensional systems (Fin n → ℝ)
is now fully proven. The proof factors into:
1. exists_forward_solution — generic lemma building a forward solution on [0,∞)
for any Lipschitz vector field via Nat.rec over τ-intervals with
HasDerivWithinAt.union at boundaries and Nat.find indexing.
2. Time reversal via f_neg (x ↦ -f x) applied to exists_forward_solution gives
the backward solution.
3. γ_full splices both halves with case split at t=0.
4. The splice point t=0 is resolved via
hasDerivAt_iff_tendsto_slope_left_right, with the left slope obtained by
composing the negative-forward slope with y ↦ -y and an algebraic identity
γ_full(y) = γ_neg_fwd(-y) on y ≤ 0.
Previously 1 sorry (the existence existence) remained; it is now closed.
The uniqueness half was already proven via ODE_solution_unique_univ.
Build: 3583 jobs, 0 errors (lake build)
This squashes all local history (768 commits) onto the scrubbed PR #90
baseline. Individual commits were lost during filter-repo corruption;
the working tree content is preserved intact.
Build: N/A (working tree state only)
Squash the four overlapping feature branches into a single change set against
main, eliminating cross-PR merge conflicts and the duplicated CI-fix scripts.
What this brings in (merge order #79 -> #80 -> #81 -> #89):
- #79 refactor(infra): shared utilities (4-Infrastructure/lib/*: q16, hashing,
jsonl, fraction_utils) + the scripts/math-first/* validators that the
math-check CI requires.
- #80 feat(lean): Semantics.E8Sidon (1025 lines) -- Eisenstein coefficient
identity E4^2 = E8 and the Sidon framework. E4_sq_eq_E8_coeff is fully proved
(all Fourier-coefficient extraction machine-checked); the single residual gap
is pinned to E4_sq_eq_E8_qExpansion (Mathlib lacks the valence formula /
dim M8 = 1). 4 sorries + 1 axiom (e8_additive_completeness), all TODO(lean-port).
- #81 refactor(lean): Float-free FixedPoint core (integer-only sqrt/log2/expNeg).
E8Sidon.lean kept at #80's final 1025-line version (the #81 intermediate
438-line copy was overridden by merge order).
- #89 feat(lean): Semantics.RRC.PolyFactorIdentity -- short-sleeve polynomial
detection at the zerocopy limb boundary; now imports Semantics.E8Sidon for
sigma3/sigma7/convolutionLHS (single source of truth) instead of inlining them.
Conflict resolution:
- flake.nix -> canonical rs-surface removal (Garnix shutdown).
- scripts/math-first/* -> byte-identical across branches, clean.
- .cursorrules / AGENTS.md -> unified; baselines + sorry inventory refreshed.
Verification:
- lake build (default aggregator): 3573 jobs, 0 errors.
- lake build Semantics.RRC.PolyFactorIdentity (E8Sidon + FixedPoint + PolyFactor):
3655 jobs, 0 errors. Witnesses verified (sigma7 4 = 16513, convolutionLHS 6 = 2350).
- Python tests: 68/68 pass.
Note: the "Workers Builds: researchstack" check is a preexisting external
Cloudflare build unrelated to this change (no branch touches 4-Infrastructure/cloudflare/).
Build: 3573 jobs (default), 3655 jobs (narrow), 0 errors
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
- Define TranslationResistance, TransportMetric, and TransportSpace
- Formalize Randers metric F = alpha + beta with Riemannian base and Lyapunov drift
- Connect to PIST via pistMass as transport cost functional
- Define IntelligenceDensity T = C/tau as system capability metric
- Provide executable witnesses for all definitions
- Follow AGENTS.md naming conventions and Q16_16 arithmetic
Build: 3561 jobs, 0 errors (lake build)
Per AGENTS.md: Lean is the source of truth. All computational gates have #eval witnesses.
- Define TranslationResistance, TransportMetric, and TransportSpace
- Formalize Randers metric F = alpha + beta with Riemannian base and Lyapunov drift
- Connect to PIST via pistMass as transport cost functional
- Define IntelligenceDensity T = C/tau as system capability metric
- Provide executable witnesses for all definitions
- Follow AGENTS.md naming conventions and Q16_16 arithmetic
Build: 3561 jobs, 0 errors (lake build)
Per AGENTS.md: Lean is the source of truth. All computational gates have #eval witnesses.
- BraidDiatCodec.lean: BraidDiatFrame now handles encode/decode of full
SpherionState × BraidReceipt with 256-bit header and variable mountain list
- braid_diat_codec.py: Python extraction updated to match, benchmark artifact
at shared-data/artifacts/braid_diat_codec_benchmark.json (714B avg vs
messagepack 1748B avg)
Build: lake build Compiler 3313 jobs, 0 errors
Implements Householder reflections for QR factorization:
- Q16Vec/Q16Mat: fixed-dimension vectors/matrices in Q16_16
- HouseholderReflection: H = I - 2vv^T/(v^T v)
- householderVector: compute reflection from column
- applyReflection: Hx = x - 2(v·x)/(v·v) * v
- qrFactorize: QR via Householder reflections
- incrementalUpdate: add column and update QR (streaming)
- quantize/quantizeVec: deterministic quantization for hashing
- O_AMMR_QRNode: QR state + basis size + hash
Key properties:
- All Q16_16 fixed-point (no Float)
- Deterministic quantization for hashing
- Incremental update for streaming spike trains
- Basis size control (rank control)
1 sorry: n > 0 precondition for householderVector
lake build: 3302 jobs, 0 errors
- IntNodeToPhaseVec_add: case analysis on all 9 coordinate-length combos
- braidCross_merge_correspondence: linear via PhaseVec.add + IntNode.add
- k_spike_step_count: structural induction on spike list
- receipt_correspondence: 6-D BraidReceipt ↔ SpherionState field mapping
- receipt_encode_stable: eigensolid encodeReceipt stability (step_count +1 only)
lake build: 3560 jobs, 0 errors
Implements the copy-if pattern as a Lean tactic:
- 'copy_if' tries rfl → decide → omega → norm_num → simp in order
- 'copy_if?' reports which closer worked (for profiling)
- Each closer is a 'zero delta' check — if goal is in normal form,
closes instantly; if not, tries next closer
This is the Lean-native equivalent of:
- Blog post: vpcompressd register-dest = 40x faster
- VCN: numpy copy-if = 3.3x faster
- Pre-filter: skip trivial theorems = 2.7x faster
- LSP: copy_if tactic = instant close for zero-delta goals
Usage:
import Semantics.CopyIfTactic
theorem foo : 1 = 1 := by copy_if
theorem bar : x + 0 = x := by copy_if
theorem baz : complex := by copy_if -- falls through to simp
3298 jobs, 0 errors. Tests pass for rfl, decide, omega, norm_num.
