RecordLayer/CellLawForced: what does force the cell law #
Category: 7-SigmaLayer (the record layer's own foundations).
TERM-SCOPE(Hamiltonian) — the vector-field sense, at the linear level; specs/TERMS.md.
CellLawFreedom.lean proves the negative half: torus invariance, normalisation, support and
measurability do not single out the moment map. This module proves the positive half, and the gap
between them is one word. sqRate is invariant under the torus action; the moment map generates
it. Generation is the moment-map equation ι_{X_i} ω = dΦᵢ, and it forces the rates.
What is proved #
★★ generatedRateField_eq_momentMap — if a bare rate field CPN N → Fin N → ℝ has rates that
are the degree-0 normalisations of Hamiltonians for the coordinate phase rotations, then they are
the moment map. Not up to a constant: exactly, with no side hypothesis at all — no ContextField
structure and not even N ≥ 2. torusGenerated_eq_momentMap is the one-line ContextField
corollary the record layer consumes.
Stating the theorem bare is deliberate, and it is the second correction this module has taken on the
same point: with sum_one and nonneg absent from the statement, no reader can misattribute the
constant-killing to them, as an earlier draft of this header did.
⚠️ Where the rigidity actually lives, because it is easy to misattribute and a first draft of
this header did. The additive constant is killed by homogeneity, not by the context field's
axioms: rate is a function of the ray, the homogenisation has degree two, so rescaling a
representative by 2 forces k = 4k. sum_one and nonneg are never used. (In the manifold
argument the division of labour is the other way — on ℂℙᴺ⁻¹ circle-Hamiltonians genuinely carry
the freedom Φᵢ + cᵢ, and there the simplex axioms are exactly what remove it. This proof enacts
that argument's shape on a linear predicate that never had the freedom.)
The chain: ★ isPhaseHamiltonian_coordEnergy (the coordinate energy ‖xᵢ‖²/2 generates the i-th
phase rotation — the instantiation of quadraticEnergy_hamiltonian_duality at the coordinate
projection); ★ IsPhaseHamiltonian.eq_coordEnergy_add (uniqueness up to an additive constant, from
is_const_of_fderiv_eq_zero on the connected model); then the two pinning steps above.
★ isTorusGenerated_momentContext — the hypothesis is inhabited, so the theorem is not vacuous.
★ sqContext_not_torusGenerated — and the rival of CellLawFreedom.lean fails it. This is a one
line consequence of the two modules together: if sqContext generated the rotations it would equal
the moment map, contradicting rate_field_not_forced_by_torus_symmetry. The freedom theorem is what
makes the forcing theorem bite.
What this settles, and at what price #
Settles: what the corpus has to assume about the cell law. specs/POSITS.md Posit 1 is
restated, not discharged — the posit count is unchanged and the honest headline is that its
quality improves: from the rates are this formula to the rates generate the phase rotations of
the measurement context's pointer torus. That is the definition of a moment map.
The gain is anti-circularity, and it is the real prize here. The old premise was a Born-shaped
formula ‖pᵢ‖²/‖p‖² feeding a derivation of Born — the very worry GlobalBasin.lean's
anti-circularity note fences off. The new premise, ι_{X_i} ω = dF, mentions no probability, no
amplitude, no Born target: it is a condition on generating a group action. The Born shape of the
rates is now derived from a non-probabilistic geometric premise.
And the premise is not a noncontextuality assumption — it is single-context, one basis, with no
cross-basis family anywhere in it. The Gleason/frame-function route, which would have cost
noncontextuality (specs/cell-law-scoping.md, stage 2), is not needed and is not taken. So
"Gleason-free" survives intact for both the volume theorem and the cell law.
⚠️ What is not settled, stated at full strength. IsTorusGenerated c is extensionally
equivalent to c.rate = momentMap — the theorem above is one direction, and
isTorusGenerated_momentContext is the other. So this is a characterisation, and the forcing is
conditional on a premise as strong as the cell law itself, differently and better expressed. Nothing
in ContextField, in the dynamics, or anywhere else in the corpus compels a context's rates to be
Hamiltonian generators of its pointer torus. Deriving that from the de-isolation dynamics is the
H_int frontier, and it is not attempted here.
Price, stated plainly. This is the linear statement, on the Hermitian model ℂᴺ with the
Kähler structure taken as given (Kahler.fundamentalForm; the pointwise triple is
IsFubiniStudyKahler). The manifold statement — that this is the moment map of the Tⁿ action on
ℂℙᴺ⁻¹ for the Fubini–Study symplectic form — remains unformalised, Mathlib having no symplectic
manifold API (MATHLIB-ABSENT(file:Mathlib/Geometry/Manifold/DifferentialForm)). ⚠️ The Kähler
and manifold structures are posited, deliberately (author decision 2026-09-04); what is proved is
that given them the rate field is forced. The descent from ℂᴺ to ℂℙᴺ⁻¹ is by explicit degree-0
homogenisation (IsTorusGenerated), not by manifold theory, so no quotient machinery is assumed.
⚠️ Updated 2026-09-08: the manifold form of the moment-map equation for the torus action now
exists — Projectivization.torusField_isHamiltonianVectorField
(Mathlib/Geometry/Manifold/Instances/ProjectiveSpaceMomentMap.lean, ι_X ω_FS = d(2 ∑ θₖ momentMap)
on ℂℙⁿ with fsForm). This module's posit and proof are unchanged — they rest on the linear-level
IsPhaseHamiltonian — and what changed is only that "Mathlib has no symplectic manifold API"
(MATHLIB-ABSENT(file:Mathlib/Geometry/Manifold/DifferentialForm), still true of Mathlib) is no
longer the reason the manifold form was absent: the corpus built its own.
Three conventions are visible in the predicate and should stay visible. IsTorusGenerated asks
for a Hamiltonian defined and differentiable on all of ℂᴺ; momentContext supplies one
(‖xᵢ‖²/2, polynomial), and since ℂᴺ ∖ {0} is connected any solution on the punctured space
extends, so this costs nothing. And the form's scale is fixed — phaseGen fixes unit-speed
rotation, fundamentalForm fixes ω u (J u) = ‖u‖². Rescaling ω ↦ λω does not produce a rival
cell law: it makes the predicate uninhabited among context fields, since sum_one rejects
λ · momentMap. (CellLawFreedom.lean records the same scale point.)
And the form's orientation: phaseGen i x = -(i · Pᵢ x) is the generator of ψᵢ ↦ e^{-iθ}ψᵢ,
the clockwise rotation — the exp(-itA) Hamiltonian-flow convention the corpus already uses in
quadraticEnergy_hamiltonian_duality. This is doing the same kind of quiet selection work as the
scale: under the mirrored convention +(i · Pᵢ x) the forced Hamiltonian is -coordEnergy, whose
normalisation is -momentMap, and no context field carries that (sum_one refutes it). So the
orientation is what picks +momentMap over -momentMap, and is recorded here rather than left
implicit.
⚠️ Constant-shifted fields momentMap + c with ∑cᵢ = 0 are circle-Hamiltonians on ℂℙᴺ⁻¹ and
fail this predicate — so it is intensionally stricter than the manifold condition. No legitimate
rival is excluded by that: every such field violates nonneg, since each momentMapᵢ attains 0.
References #
RecordLayer/CellLawFreedom.lean (sqContext, rate_field_not_forced_by_torus_symmetry — the
negative half this module completes); RecordLayer/GlobalBasin.lean (ContextField,
momentContext, globalBasin_born); Mathlib/Analysis/InnerProductSpace/HamiltonianVectorField.lean
(quadraticEnergy_hamiltonian_duality, hamiltonianVectorFieldOf, fundamentalForm);
LF4/MomentMap.lean (momentMap_mk, euclidean_norm_sq_eq_sum); LF4/KahlerOnticSetup.lean
(IsFubiniStudyKahler — the posited structure); specs/POSITS.md (Posit 1, restated here — not discharged);
specs/cell-law-scoping.md (why the frame-function route was declined);
specs/future-work.md ("Cell-law characterisation"); specs/TERMS.md (Hamiltonian, two senses).
The coordinate projection and its energy #
CSD-free linear algebra; an upstream candidate alongside HamiltonianVectorField.lean.
The i-th coordinate projection, as a continuous linear map.
Equations
Instances For
The i-th coordinate energy ‖xᵢ‖²/2 — the quadratic energy of the i-th projection.
Instances For
The coordinate energies sum to half the squared norm — the identity that will pin the
constants against ContextField.sum_one.
Generating the phase rotation #
The generator of the i-th coordinate phase rotation, -(i · Pᵢ x).
Equations
- CSD.RecordLayer.phaseGen i x = -(Complex.I • (CSD.RecordLayer.coordProj i) x)
Instances For
F is a Hamiltonian for the i-th phase rotation: ι_{X_i} ω = dF. This is the
moment-map equation, at the linear level, and it is the property sqRate lacks.
Equations
- CSD.RecordLayer.IsPhaseHamiltonian F i = (Differentiable ℝ F ∧ ∀ (x v : EuclideanSpace ℂ (Fin N)), Kahler.fundamentalForm (CSD.RecordLayer.phaseGen i x) v = (fderiv ℝ F x) v)
Instances For
★ The coordinate energy generates the phase rotation. The instantiation of
quadraticEnergy_hamiltonian_duality at the coordinate projection — the ingredient the linear
Hamiltonian layer had and never used.
★ Uniqueness up to an additive constant. Two Hamiltonians for the same vector field have
equal differentials, and ℂᴺ is connected, so they differ by a constant.
The cell law, forced #
A context field is torus-generated when its rates are the degree-0 normalisations of Hamiltonians for the coordinate phase rotations — i.e. when they are moment coordinates.
This is the hypothesis that does the work, and it is the one sqContext fails: invariance under
the torus is weaker than generating it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same condition on a ContextField.
Instances For
★ The hypothesis is inhabited — the moment-map field is torus-generated, so the forcing theorem below is not vacuous.
★★ The cell law is forced, given generation — stated for a bare rate field, because
that is the honest strength. Any function CPN N → Fin N → ℝ whose rates generate the coordinate
phase rotations is the moment map: exactly, not up to a constant, with no ContextField in
sight and no cardinality hypothesis.
The additive freedom left by IsPhaseHamiltonian.eq_coordEnergy_add is removed by homogeneity:
the rate is a function of the ray while the homogenisation has degree two, so rescaling a
representative by 2 forces k = 4k. ⚠️ Stating this for a bare rate field is deliberate. An
earlier draft credited the constant-killing to sum_one and nonneg, which was a misreading of
the proof route; with those axioms absent from the statement the misreading is no longer
available.
With CellLawFreedom.rate_field_not_forced_by_torus_symmetry this locates the boundary precisely:
torus invariance leaves a continuum of rate fields, torus generation leaves exactly one.
★★ The cell law is forced, given generation — the ContextField form, for the record
layer's consumers. A one-line corollary of the bare-rate-field theorem above, which is where the
mathematics is.
★ The rival cell law fails the generating condition. sqContext matches the moment map on
every property the corpus verifies of it and is still not it, so by the forcing theorem it cannot
generate the phase rotations. The freedom theorem is exactly what makes this a one-line
consequence — the two modules are one argument.