Research-Stack/0-Core-Formalism/lean/Semantics/AGENTS.md

AGENTS.md - Lean/Semantics

Scope: 0-Core-Formalism/lean/Semantics/

The strict operating rules live in ../../../6-Documentation/docs/AGENTS.md. Follow those rules for all Lean, proof, fixed-point, hardware-extraction, and shim-boundary work.

Local Rules

• Keep module names aligned with file names and namespaces.
• Prefer small domain modules over utility files.
• Every new computational gate needs an executable witness: theorem, #eval, or native-decision proof.
• Run the narrow build target first, for example:

lake build Semantics.BeaverMaskFreshness

• Run the broader build before claiming a stable Lean surface:

lake build

• Do not delete difficult theorems to make builds pass. Fix proofs or quarantine with an explicit TODO(lean-port): ... boundary.
• Treat generated Python, Rust, Verilog, and JSON as shims or receipts, not as the formal source of truth.
• Float (Q16_16.ofFloat, Q0_16.ofFloat, Q0_64.ofFloat) is forbidden in compute-path code. Use Q16_16.ofNat, Q16_16.ofRatio, or Q16_16.ofInt instead. As of 2026-06-15, the core Semantics.FixedPoint module is fully Float-free: ofFloat/toFloat live in Semantics.FixedPointBoundary and must only be imported at I/O boundaries. Q16_16.sqrt, Q16_16.log2, Q16_16.expNeg, and Q0_16.log2 use integer-only algorithms (Newton's method, bit-position extraction, piecewise-linear approximation).
• Every new compressor theorem pair MUST provide both eigensolid_convergence and receipt_invertible. The convergence theorem proves the crossing loop stabilizes; the invertibility theorem proves the receipt bijectively encodes the original state including zero/gap/timing/absence dimensions.
• The BraidEigensolid module (Semantics.BraidEigensolid) is the canonical compressor target (planned, not yet written): 10 sections covering Q0_2 crossing matrix, Sidon labels (powers of 2), golden centering (φ⁻¹ = 0x9E70), eigensolid convergence, receipt invertibility, and Anti-BraidStorm adversarial check. The fixed-point constructor patterns in BraidCross and BraidStrand must compile first.
• Receipt invertibility is a stronger theorem than convergence. Convergence says crossStep(crossStep(s)) = crossStep(s). Invertibility says the full receipt (C, sidon, k, ε_seq, t, ∅_scars) bijectively reconstructs s and that decode(encode(s)) = s holds for all valid inputs.
• enwik9 is the end-to-end test vector. The hierarchical compressor (bytes→chunks→banks→file) must prove decode(encode(enwik9)) = enwik9 byte- for-byte via a Lean execution witness.

Current Stack-Solidification Anchors

• Semantics.BeaverMaskFreshness is a finite admission gate for Beaver-mask freshness negative controls.
• Semantics.HCMMR.Kernels.EntropyCollapseDetector is the finite arithmetic receipt for the corrected entropy-collapse detector. It intentionally keeps logarithmic/Hurst quantities as scaled receipt constants and proves the dense-rank crossing count, D2 numerator, and Kendall tail values with executable Lean checks.
• Stack status receipts live under shared-data/data/stack_solidification/.
• The canonical arithmetic note is ../../../6-Documentation/docs/distilled/ArithmeticSpec_Corrected_2026-05-11.md. Treat sigma_q on n=8 as a deterministic window feature, not as a robust Hurst estimator.
• The K=21 prime-gap rerun receipt is ../../../shared-data/data/stack_solidification/prime_gap_k21_rerun_receipt_2026-05-11.md. Its conclusion is deliberately bounded: rare surviving windows are candidate motifs, not a general prime-gap collapse theorem.
• Historical staged slices are documented in ../../../6-Documentation/docs/stack_solidification_staging_manifest_2026-05-09.md and ../../../6-Documentation/docs/stack_solidification_staging_manifest_2026-05-10.md.

Local Quarantine Boundaries

• The root .gitignore excludes known local formal scratch/WIP such as 2-Search-Space/FAMM/FAMM_FSDU.lean and 4-Infrastructure/hardware/test.lean. Do not revive ignored Lean files into the clean build surface without first making them compile under a narrow target.
• Generated *_tb.v and *_test_vectors.json files are build artifacts unless a task explicitly promotes one as a hardware receipt.

Blessed Compiler Surface (as of 2026-05-30, commit b7f3d1a9)

The Compiler lean_lib in lakefile.toml gates the promoted API surface. Only the following roots are blessed for downstream import and receipt emission:

Root	Purpose
Semantics.RRC.Emit	Alignment classifier; emitCorpus generic entry point
Semantics.AVMIsa.Emit	Sole output boundary — AVM canaries + stamps all receipts
Semantics.RRC.Corpus278	278-equation raw feature list (Python-supplied, Lean-gated)

Build the narrow surface with:

lake build Compiler

Build the full workspace with:

lake build

Compiler surface baseline: 3313 jobs, 0 errors (lake build Compiler, commit 859d8726, reverified 2026-05-28). Full workspace: 3573 jobs, 0 errors (lake build, reverified 2026-06-15). PistSimulation: 3309 jobs, 0 errors (lake build Semantics.PistSimulation, commit 778b78d3, reverified 2026-05-27). EmergencyBoot: 3302 jobs, 0 errors (lake build Semantics.Hardware.EmergencyBootTypes Semantics.Hardware.EmergencyBootState Semantics.Hardware.EmergencyBootShell, reverified 2026-05-27).

Float-Free FixedPoint Architecture (as of 2026-06-15)

FixedPoint.lean (968 lines) is now fully Float-free. Core compute functions use integer-only algorithms:

Function	Algorithm	Location
natLog2	Fuel-based bit-shift loop (64 steps)	FixedPoint.lean:30
intSqrt	Integer Newton's method (64 iterations)	FixedPoint.lean:43
Q16_16.sqrt	intSqrt(q.raw * 65536)	FixedPoint.lean:316
Q16_16.log2	Bit extraction + linear interpolation (94548 = 1/ln2 in Q16.16)	FixedPoint.lean:324
Q16_16.expNeg	7-segment piecewise-linear, max error ~0.02	FixedPoint.lean:336
Q0_16.log2	Bit extraction (47274 = 1/ln2 in Q0.16)	FixedPoint.lean:130

Removed from core: ofFloat, toFloat, ln, pow, sin, log (Q16_16); toFloat, ofFloat (Q0_16); q0_64ScaleFloat, ofFloat, toFloat (Q0_64).

FixedPointBoundary.lean (89 lines) quarantines Float conversions at the I/O boundary. 14 downstream files import it for display/JSON purposes: FuzzyAssociation, Autobalance, ProvenanceSource, Tape, Q16_16Numerics, CGAVersorAddress, EfficiencyAnalysis, Functions/BracketedCalculus, LocalDerivative, NUVMATH, QFactor, SLUG3, SubagentOrchestrator, ExtensionScaffold/Compression/SignalPolicy, LawfulLoss.

E8Sidon Module (as of 2026-06-15)

E8Sidon.lean (1025 lines) formalizes the Eisenstein coefficient identity and Sidon set infrastructure:

• sigma3, sigma7, convolutionLHS — divisor sum definitions with 15 #eval witnesses
• bernoulli_four, bernoulli_eight — B4 = B8 = -1/30 via native_decide
• E4_normalization, E8_normalization — -(2k/Bk) = 240, 480
• E4_sq_eq_E8_coeff — fully proved; all coefficient extraction is machine-checked, with the single residual gap pinned to E4_sq_eq_E8_qExpansion (E₄² = E₈ as q-expansions; blocked on Mathlib valence formula / dim M₈ = 1)
• IsSidonSet, sidon8 (card=8), Sidon energy bounds, greedy extraction
• 4 sorries total (down from 12), all with TODO(lean-port) + proof sketches: E4_sq_eq_E8_qExpansion, collision_excess_decrease, greedy_sidon_extraction, e8_singer_improvement
• 1 axiom (e8_additive_completeness) — open problem in additive combinatorics

PolyFactorIdentity Module (RRC short-sleeve detection, as of 2026-06-15)

Semantics/RRC/PolyFactorIdentity.lean (390 lines) hooks the zerocopy limb boundary as a structural flag for sparse ("short-sleeve") polynomial blocks:

• import Semantics.E8Sidon — reuses the authoritative sigma3/sigma7/convolutionLHS (single source of truth; the earlier standalone inlined defs were removed once E8Sidon landed in the tree)
• limbDecompose, shortSleeveDetected, polyDecomposabilityScore, zeroCopyScan with 27+ #eval witnesses
• 3 sorries (limbDecompose_polyEval_roundtrip, zeroLimbs_bound_terms, shortSleeve_mono_zero_prepend), all TODO(lean-port) with proof sketches
• Verified narrowly: lake build Semantics.RRC.PolyFactorIdentity — 3655 jobs, 0 errors

BraidDiatCodec — chirality/MMR/braid residual codec

New codec module (Semantics.BraidDiatCodec) layers the mountains-on-mountain stack into a compact binary format:

• Layer 1 — ChiralityDIAT: 2-bit chirality + 62-bit DIAT slot address. Encode: (Chirality × UInt32) → ChiralityDIAT. Decode roundtrip proven (encode_decode_roundtrip).
• Layer 2 — MountainPacked: height(8) + apex(48) + base_count(8) + base coords. Lossless fromMountain / toMountain with inner MMR preserved recursively.
• Layer 3 — BraidResidualPacked: 5 Q0_2 fields × 2 bits = 10 bits per crossing residual. Q0_2 roundtrip proven (bracket_roundtrip).
• Layer 4 — BraidDiatFrame: 256-bit fixed header + variable mountain list. Full encode / decode between SpherionState × BraidReceipt and frame.

Key invariants: DIAT mass (a + b = 2k + 1), MMR strictly decreasing heights, Q0_2 4-state packing.

BraidSpherionBridge — SpherionState ↔ BraidState equivalence

New bridge module (Semantics.BraidSpherionBridge) wires the mountains-on-mountain formalism to the braid strand formalism:

• SpherionSpike — spike(m : Mountain, crossPair : Fin 4) ties a Mountain to which braid pair fires
• spikeToStrandUpdate — applies a spike's crossing to a BraidState via braidCross
• strandFlow — iterates spikeToStrandUpdate over a spike train
• braidCross_merge_correspondence — (admit) braidCross on (i,j) ↔ Mountain.merge for corresponding pair
• receipt_correspondence — (admit) BraidReceipt = SpherionState receipt dimensions

Key remaining admits: IntNodeToPhaseVec linearity (IntNode.add ↔ PhaseVec.add), step count accumulation, full receipt dimension mapping.

goldenContractionEnergyDecrease — proof status

Statement: For Burgers fields with non-negative u and pointwise contraction u'[i] ≤ u[i], the golden-contraction dissipation step reduces kinetic energy.

Status: Formal proof complete. The proof lifts pointwise square inequalities through a List.Forall₂ fold induction and uses Array.foldl_toList only to connect the array energy definition to the list proof.

Current theorem hypotheses: h_u_nonneg, h_u'_nonneg, h_pt (pointwise u'[i] ≤ u[i]), h_size, hN. Convexity is not part of this theorem; it belongs in a separate premise-discharge lemma for h_pt and h_u'_nonneg.

Architecture: AVM is the sole output boundary

RRC.Corpus278   — 278 FixtureRows, raw features only (no decisions)
      ↓ emitCorpus
RRC.Emit        — alignment gate (missingPrediction / alignedExact / etc.)
      ↓ emitRrcCorpus278
AVMIsa.Emit     — AVM canaries must pass; stamps avm.rrc_corpus278.bundle
                  emits final JSON; SOLE output boundary

Rule: Nothing outside AVMIsa.Emit may emit a top-level receipt JSON. RRC.Emit is a classifier that feeds it. RRC.Corpus278 supplies raw features.

Goal A canary receipt (AVMIsa.Emit §1–6)

Three passing canaries: avm.canary.not, avm.canary.and, avm.canary.or. Expected #eval emit.json shape:

{
  "schema": "avm_canary_emit_v1",
  "all_canaries_passed": true,
  "receipts": [...],
  "rrc_logogram": { "shape": "logogramProjection", ... },
  "projection_passed": true
}

278-equation corpus (AVMIsa.Emit §7 / RRC.Corpus278)

emitRrcCorpus278 classifies all 278 rows and stamps the bundle. Expected #eval corpus summary: (278, <passed>, 278 - <passed>).

Current state: (278, 0, 278) — all held, no PIST labels present yet. This is correct and honest — the gate reports exactly what it sees.

The PIST predictions merge pipeline: pist_matrix_builder.py → rrc_pist_predictions_278_v1.json → build_corpus278.py reads it and populates pistProxyLabel/pistExactLabel in generated Corpus278.lean. The merge is keyed by invariant_receipt.object_id (equation_id = rrc_eq_<hex>). When the predictions artifact has non-null labels, regenerating Corpus278.lean via python3 4-Infrastructure/shim/build_corpus278.py will automatically flow them into determineAlignment — no Lean emit logic changes needed.

Each row carries 5 generator fields for EN9wiki page generation:

• operatorTokens — domain/operator token list (from route_hint + rrc_kind)
• invariantsDeclared — declared invariant family (from domain_type)
• boundaryConds — binding class (from bind_class)
• templateKey — page-generator template (definition/master_equation/gate/receipt/hold)
• templateParams — compact rendering parameter string

To regenerate Corpus278.lean from source:

python3 4-Infrastructure/shim/build_corpus278.py

Python's role: raw feature extraction only. Lean's role: all gating decisions.

Quarantined Modules (not in build surface)

Module	File	Reason
PIST.HybridTSMPISTTorus	2-Search-Space/PIST/HybridTSMPISTTorus.lean	2 sorry-related errors; no importers

Quarantined files are excluded from lakefile.toml PIST roots. Revive only after narrowly compiling the file under a scratch target.

Pending Proof Work

• Semantics.E8Sidon — E₈ lattice Sidon framework (new module). 4 sorry tokens across 4 theorems (down from 12), all with TODO(lean-port).
  • E4_sq_eq_E8_qExpansion: the single irreducible Mathlib gap — E₄² = E₈ as q-expansions. Blocked on dim M₈(SL₂ℤ) = 1 / valence formula, absent in Mathlib v4.30 (LevelOne.lean proves Module.rank only for weight ≤ 0 and carries an explicit "TODO: Add finite-dimensionality"). This is the only residual gap in the whole E₄²=E₈ chain.
  • collision_excess_decrease, greedy_sidon_extraction, e8_singer_improvement: Finset/infrastructure-heavy, with proof sketches.
  • 1 axiom: e8_additive_completeness (open problem in additive combinatorics).
  • E4_sq_eq_E8_coeff is now fully proved: the entire Fourier coefficient extraction (E₄ coeff = 240·σ₃, E₈ coeff = 480·σ₇, constant term 1, antidiagonal coeff_mul split into 480·σ₃ boundary + 240²·convolutionLHS middle, then exact_mod_cast ℂ→ℕ) is machine-checked, reducing it to E4_sq_eq_E8_qExpansion. Computationally verified for n = 2, 3, 4 via #eval.
  • r8_via_sigma3, r8_one are now fully proved after the r8 definition fix (r8 n = 240·σ₃(n) matching Θ_{E₈} = E₄, was incorrectly 480·σ₇).
  • Fully proved: sidon_iff_zero_collision (both directions via double-inclusion
    • cardinality squeeze), erdos30_e8_conditional (Erdős–Turán bound via difference injection + trichotomy partition), sidon_energy_bound, sidon_diff_injective, greedy_sidon_sqrt, fiber_partition, e8_levelset_density, exists_collision_witness.
  • Definitions (sigma3, sigma7, convolutionLHS, IsSidonSet, r8) and Bernoulli evaluations (bernoulli_four, bernoulli_eight) fully proven.
• Semantics.RRC.PolyFactorIdentity — RRC short-sleeve detection at the zerocopy limb boundary. Imports Semantics.E8Sidon for sigma3/sigma7/convolutionLHS (single source of truth). 3 sorries, all with TODO(lean-port) + proof sketches:
  • limbDecompose_polyEval_roundtrip: zerocopy limb view round-trips polynomial eval.
  • zeroLimbs_bound_terms: zero-limb count bounds the active-term count.
  • shortSleeve_mono_zero_prepend: prepending a zero limb preserves short-sleeve flag.
• goldenContractionEnergyDecrease is discharged. Remaining follow-up is a separate premise-discharge lemma showing when the Burgers golden-contraction step satisfies h_pt and h_u'_nonneg.
• HyperbolicStateSurface.ko_preserves_hyperbola_approx: former sorry replaced by explicit premise onHyperbolaApprox (forwardStep s Δu) Q16_16.epsilon (line 69). Remaining: TODO(lean-port) discharge that premise from a formal Q16_16.sqrt error-bound lemma.
• SSMS.aciPreservedByMlgruStep: theorem signature updated with h_ft_range : ∀ i, (fT i).toInt ≥ 0 ∧ (fT i).toInt ≤ FixedPoint.q16Scale (line 546). The hprev and hcand sub-proofs use abs_sub_comm with correct argument ordering (lines 559–571). The f_eps and omf_eps sub-lemmas are proved via mul_mono_left + one_mul (PROVED, lines 605–607, 611–614). The omf_toInt equality is proved via q16Clamp_id_of_inRange (lines 575–599). The remaining admit (line 619) is the full mlgruStep preservation chain: triangle inequality + mul bounds → H.aciBound. Requires abs_triangle and abs_mul_le to be proved in FixedPoint.lean.
• FixedPoint.lean Q16_16 lemma library (lines 617–695):
  • mul_mono_left/right ✅ PROVED — Int.ediv_le_ediv hpos hmul pattern works with explicit hpos : 0 < q16Scale proof
  • abs_sub_comm ✅ PROVED — three-case split on d := a.val - b.val relative to q16MinRaw/q16MaxRaw bounds
  • sub_eq_add_neg (line 620): admit, unused
  • add_le_add (line 652): admit, unused
  • abs_nonneg (line 659): admit, unused
  • abs_mul_le (line 665): admit, unused
  • abs_triangle (line 674): admit, needed for SSMS preservation chain
• EmergencyBootTypes.lean — 6502 design philosophy hardware types (graphene memristor, optical fiber hot/cold paths, voltage differential computation). All structures compile; remaining formal work: eigensolid_convergence for optical delay-line memory, receipt_invertible for geometric seed extraction.
• EmergencyBootState.lean — power failure detection, seed assembly, self-sufficiency checks. Verified: utilizationWithinBounds (FPGA resource limits), powerFailureMonotonic (bridge isolation implies no false detection).
• EmergencyBootShell.lean — Tiny IP command interface (BOOT, SCAN, STATUS, EXIT, etc.). Verified: commandOpcode_roundTrip (opcode parsing correctness). TODO(lean-port): status byte round-trip theorem, phase-disjointness for command gating.

Key API Notes (Lean 4.30 / this workspace)

• Q16_16 is a Subtype { x : Int // q16MinRaw ≤ x ∧ x ≤ q16MaxRaw }. Safe constructors: Q16_16.ofRawInt (n : Int), Q16_16.ofBits (u : UInt32), Q16_16.ofNat, Q16_16.ofRatio. No struct literals { val := N }. Float constructors (ofFloat/toFloat) are only in FixedPointBoundary.lean.
• Q0_16 has add/sub (no addSat/subSat). log2 is integer-only (bit extraction). Float conversions are in FixedPointBoundary.lean.
• List.get? does not exist — use list[i]? subscript syntax.
• liftMetaM is the correct combinator for MetaM → TacticM in mapM.
• MVarId.toNat does not exist — use g.name.toString.
• List.size → .length; Json.num Nat → Json.num { mantissa := (n : Int), exponent := 0 }.

Cross-References

See root AGENTS.md for:

• Post-Interaction Workflow (mandatory 5-step session-end procedure)
• Programming Choice Flow (Lean owns decisions; Python owns I/O)
• Do Not Sweep rules (no broad git add .)
• Git Remote Hygiene