IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumBinding
Samples continuum phase and lapse fields onto the cyclic lattice Z/nZ at nodes j/n, and identifies the continuum lattice bracket with the periodic sampled dynamic structure bracket. Gap-5 / Dirac-algebra continuum workers cite it when wiring the rate-h continuum residual to the general-n HamDyn bracket. The argument is reindexing and wraparound identities on ZMod, plus equality of the two bracket presentations.
claimContinuum phase and lapse fields are sampled on $\mathbb{Z}/n\mathbb{Z}$ at nodes $j/n$. The continuum lattice bracket equals the periodic sum of dynamic-structure bracket samples, and the general-$n$ Hamiltonian dynamic bracket coincides with that periodic sampled sum (no boundary term under wraparound).
background
This module sits in the Gravity SevenGaps campaign, Wave C2 R4: binding the continuum Dirac-algebra residual to the discrete dynamic structure bracket on a cyclic lattice.
Upstream, DiracAlgebraContinuum packages the sampled-lapse Wronskian rate-$h$ residual (named open in the weighted structure-sum limit) with the lattice RHS shape and the dynamic structure profile as the continuum-limit object. DynamicStructureBracketN generalizes the two-site HamDyn bracket and its self-bracket identity to arbitrary $n$ with $\mathrm{NeZero},n$: same Fréchet bookkeeping, Kronecker collapse, and periodic reindex; ZMod wraparound supplies periodicity so there is no boundary term.
The binding layer introduces sampled phase/lapse at $j.\mathrm{val}/n$, a successor wrap on the lattice, the periodic sampled dynamic-bracket sum, and the continuum lattice bracket as the continuum-side presentation of that sum.
proof idea
Definition layer first: sample continuum fields at lattice nodes, define wrap-successor, the periodic sampled bracket sum, and the continuum lattice bracket.
Supporting ZMod facts: value-of-lt, wrap-successor bounds, successor valuation, and equality of a sum over ZMod with the corresponding finite range sum.
Main equalities: the general-$n$ HamDyn bracket equals the periodic sampled dynamic bracket (by the DynamicStructureBracketN pattern under periodic reindex); the continuum lattice bracket equals that same periodic sum. A unit-periodicity helper closes the wraparound bookkeeping. No analytic limit is proved here; the module is the discrete identification layer.
why it matters in Recognition Science
Closes the discrete-to-sampled bridge needed before gap-5 continuum algebra can be audited and residual-DAG-closed.
Feeds DiracAlgebraContinuumBindingAudit (headline theorems must print inside propext / Classical.choice / Quot.sound only). Feeds Gap5ConstraintCloseStatus, which binds full-theory gap5 constraint-recovery true and flips the continuum-algebra / HKT-open ledger flags false. Feeds Gap5ConstraintResidualDAG, which names residuals for dynamic Dirac structure functions and HKT rigidity along the Wave C2/D plan.
In the RS gravity stack this is infrastructure for the continuum Dirac structure side of gap-5 constraint recovery, not a mass or alpha claim.
scope and limits
- Does not prove the continuum rate-h limit or discharge the open residual in weightedStructureSum_tendsto.
- Does not establish HKT rigidity or flip gap5 ledger Bools by itself.
- Does not treat non-cyclic lattices or boundary terms outside ZMod wraparound.
- Does not specialize to n=2 only; equalities are stated for general NeZero n.
- Does not introduce new physical constants or mass-ladder claims.
used by (3)
depends on (2)
declarations in this module (17)
-
def
sampledPhasePoint -
def
sampledLapse -
def
wrapSucc -
def
periodicSampledDynamicBracketSum -
def
continuumLatticeBracket -
lemma
zmod_val_of_lt -
lemma
wrapSucc_lt -
lemma
zmod_succ_val -
lemma
sum_zmod_eq_sum_range -
theorem
bracket_HamDynN_eq_periodicSampled -
theorem
continuumLatticeBracket_eq_periodic -
def
Periodic1 -
lemma
wrapSucc_eq_succ_or_zero -
theorem
periodicSampled_eq_sampled_of_periodic -
theorem
scaled_continuumLatticeBracket_eq_scaled_sampled -
theorem
dirac_algebra_continuum_limit -
theorem
dirac_algebra_continuum_limit_hamDynN