module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumMagnitudeBridge`

Houses the residual physical premise of the Gap-5 momentum-magnitude bridge: per-orbit energy equals cost on the two-site ledger chart. Gravity and quantum-gravity workers cite it when discharging the kinetic half of momentum additivity into the EnergyEqualsCost derivation. The module packages orbit coverage, kinetic positivity on open and closed positive quadrants, and the implication chain from energy-equals-cost to vanishing balance on the positive diagonal.

claimOn the two-site ledger chart carrier, the residual premise asserts that for each orbit the energy functional equals the recognition cost. Kinetic positivity holds on the open and closed positive quadrants; energy-equals-cost implies the kinetic condition there; and balance vanishes on the positive diagonal whenever energy equals cost.

background

Gap 5 in the Seven Gaps gravity track concerns momentum observables on a ledger chart. The chart carrier is $\mathbb{R}\times\mathbb{R}$ (two ledger sites). Upstream, momentum additivity under ledger consolidation is proved from three named properties, the first of which is the kinetic condition: pointwise $|p|=|\mathrm{imbalance}|$, i.e. the magnitude half of the momentum-magnitude bridge.

The companion import supplies the dynamic structure-function bracket on two sites (Wave C2 residuals R0+R1). That work shows a naive frozen-Hamiltonian substitution fails: the configuration partial picks up an uncompensated $\partial g/\partial q$ term. The present module isolates the remaining physical premise that links cost to energy per orbit, rather than reopening the bracket algebra.

Sibling material introduces orbit projections and coverage, elementary identities ($e^{\pm(\log\cdot)/2}$, square-root product/quotient), and the named predicates EnergyEqualsCost together with kinetic positivity on the open and closed positive quadrants.

proof idea

Not a single theorem wrapper. The module assembles supporting lemmas around the residual premise: orbit first/second projections and coverage; algebraic identities for exponential-of-half-log and square-root rearrangements; kinetic positivity statements on open and closed positive quadrants; the implication that energy-equals-cost yields kinetic positivity on the open positive quadrant; and vanishing of balance on the positive diagonal under energy-equals-cost. Downstream derivation then treats EnergyEqualsCost as the single extra input that discharges the bridge.

why it matters in Recognition Science

Feeds Gap5EnergyEqualsCostDerivation, whose verdict is that EnergyEqualsCost is independent of the Hamiltonian data (a no-go by polarization independence) and that the premise discharges from exactly one extra input. That closes the Hamiltonian lead negatively while keeping the constructive corollary: once per-orbit energy-equals-cost is granted, the kinetic magnitude half of the momentum bridge is available for the Track B additivity package.

In the Recognition gravity stack this is the residual physical hinge between ledger cost and chart momentum magnitude, sitting after the dynamic bracket residuals and before the energy-equals-cost derivation. It does not itself force the full mass ladder or the T0-T8 chain; it only packages the Gap-5 magnitude premise those later gravity closures consume.

scope and limits

Does not prove EnergyEqualsCost from Hamiltonian data alone (downstream no-go).
Does not establish full momentum additivity; only the magnitude-bridge residual premise.
Does not reopen or repair the dynamic structure-function bracket residuals R0+R1.
Does not claim global kinetic positivity off the positive quadrants or off covered orbits.
Does not derive mass-ladder, phi-fixed-point, or D=3 forcing results.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap5EnergyEqualsCostDerivation module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivity module_import

declarations in this module (32)

lemma sum_zmod2 L64
def EnergyEqualsCost L74
def KineticOnOpenPositiveQuadrant L77
def KineticOnClosedPositiveQuadrant L80
theorem exp_log_div_two L85
theorem sqrt_mul_sqrt_div L96
theorem exp_neg_log_div_two L111
theorem orbit_fst L120
theorem orbit_snd L124
theorem orbit_coverage L132
theorem energy_equals_cost_implies_kinetic_on_open_positive L147
theorem balance_vanishing_on_positive_diagonal_of_energy_equals_cost L157
theorem continuous_imbalance L168
theorem kinetic_extends_to_closed_positive_quadrant L172
theorem energy_equals_cost_continuous_implies_kinetic_on_closed L203
theorem swap_odd_preserves_kinetic_pointwise L211
theorem swap_maps_open_positive_to_itself L217
theorem orbitPoint_nonneg L222
theorem negative_quadrant_not_on_orbit L228
theorem hamDyn_decoy_value L239
theorem hamDyn_gradient_sector_nonzero_at_zero_momenta L257
theorem Jlog_ne_half_sq L268
theorem chart_product_sq_form L321
theorem exact_cost_profile_recovers_chart_product L337
theorem energy_equals_cost_of_imbalance L356
theorem chart_product_fails_for_imbalance_at_unit_lam L364
theorem orbitPoint_pos L386
theorem open_positive_kinetic_iff_energy_equals_cost L396
theorem two_imbalance_fails_energy_equals_cost L413
theorem two_imbalance_package L440
structure MomentumMagnitudeBridgeVerdict L461
theorem momentumMagnitudeBridgeVerdict L514