IndisputableMonolith.Gravity.SevenGaps.Gap5EnergyEqualsCostDerivation
Discloses the Casimir Hamiltonian model on the chart carrier LedgerState: split-torus recognition dynamics (diagSL) is the Hamiltonian flow of H = casimir/2 under the σ = 0 area form. Gravity and RS auditors cite it when tracking the EnergyEqualsCost residual in Gap 5. The module builds the Hamiltonian vector field, shows the orbit is its flow, relates Poisson imbalance to the frame determinant, and packages the imbalance and nlP momentum statements.
claimOn the chart carrier with the $\sigma=0$ area form of the symplectic cost action, the split-torus recognition dynamics is the Hamiltonian flow of $H(z)=\mathrm{casimir}(z)/2$, with identity carrier map. The module also records the Poisson imbalance identity, constancy of $H$ on orbits, and the named packages linking imbalance and non-linear momentum to the EnergyEqualsCost premise.
background
Gap 5 in the Seven Gaps gravity stack concerns the kinetic condition $p(z)^2 = \mathrm{imbalance}(z)^2$ on ledger states. The upstream momentum-magnitude bridge states that this global condition is not derived from substrate structure; on the open positive quadrant it is exactly equivalent to the named premise EnergyEqualsCost $p$. That residual remains open to discharge.
This module sits one step downstream and supplies the Hamiltonian model used to talk about that residual. The carrier is LedgerState with the $\sigma=0$ area form from Cost.SymplecticAction. The dynamics is the split-torus recognition flow diagSL. The claimed generating function is the Casimir Hamiltonian $H(z)=\mathrm{casimir}(z)/2$, with identity carrier map on the chart.
Supporting objects include the orbit Hamiltonian, its Hamiltonian vector field, a linearized Poisson bracket, and derivative facts for the half-exponentials that parametrize the flow. Poisson imbalance totals are identified with the frame determinant, giving a concrete symplectic reading of the imbalance that enters EnergyEqualsCost.
proof idea
Definition-and-derivation module, not a single theorem. It introduces orbitHamiltonian and hamiltonianVectorField, proves the orbit point is the Hamiltonian flow of $H=\mathrm{casimir}/2$, and shows $H$ is constant along orbits. Derivative lemmas for $\exp(\pm t/2)$ feed the flow calculation. Poisson imbalance is computed and equated to the frame determinant. Two packages (imbalance_momentum_package, nlP_momentum_package) and a negative statement not_energyEqualsCost_nlP record what the Hamiltonian picture does and does not force about EnergyEqualsCost.
why it matters in Recognition Science
Feeds Gap5MomentumAdditivityComposition, whose consumer energyEqualsCost_of_additive_continuous_balanced_unit already shows that continuous additive balanced unit momentum implies EnergyEqualsCost. The downstream module's verdict is that unconditional additivity (b) and its constructive corollary (c) land, while (a) is refuted by a no-go. This Casimir Hamiltonian disclosure is the MODEL layer those composition-law attacks sit on: it makes precise which symplectic generator is being assumed when one talks about imbalance, Poisson structure, and the EnergyEqualsCost residual left open by the momentum-magnitude bridge. Within the gravity domain it is scaffolding for closing or sharply bounding Gap 5, not a claim that EnergyEqualsCost follows from substrate alone.
scope and limits
- Does not derive EnergyEqualsCost from substrate structure alone.
- Does not close the global kinetic gap $p^2=\mathrm{imbalance}^2$ for all ledger states.
- Does not claim the Casimir Hamiltonian is forced; it is a disclosed MODEL.
- Does not establish unconditional momentum additivity (that is downstream).
- Does not alter the $\sigma=0$ area form or replace the identity carrier map.
used by (1)
depends on (1)
declarations in this module (21)
-
def
orbitHamiltonian -
def
hamiltonianVectorField -
def
poissonLin -
theorem
hasDerivAt_exp_half -
theorem
hasDerivAt_exp_neg_half -
theorem
orbitPoint_is_hamiltonian_flow -
theorem
orbitHamiltonian_constant_on_orbit -
theorem
poisson_imbalance_total -
theorem
poisson_imbalance_total_eq_frame_det -
theorem
not_energyEqualsCost_nlP -
theorem
imbalance_momentum_package -
theorem
nlP_momentum_package -
theorem
energyEqualsCost_independent_of_hamiltonian_data -
theorem
energyEqualsCost_of_additive_continuous_balanced_unit -
theorem
energyEqualsCost_iff_pointwise_ratio_cost -
theorem
orbitPoint_eq_zero_of_nonpos -
theorem
neg_orbit_coverage -
theorem
imbalance_sq_eq_two_casimir_jcost -
theorem
quadrant_signs -
structure
EnergyEqualsCostDerivationVerdict -
theorem
energyEqualsCostDerivationVerdict