module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap5ReparamAttackOnConstraintSector`

Module for Gap 5's reparametrization attack on the gravity constraint sector: any cost that obeys the Recognition Composition Law is forced to unit weight, so power and oscillatory reparams cannot evade the canonical J-cost. Gravity workers cite it when closing free chart/weight freedom before extracting chart-invariant ratios. The argument routes J through the repo cosh-addition identity and then runs generic unit-weight forcing on the composition law.

claimThe canonical cost $J(x)=(x+x^{-1})/2-1$ satisfies the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Any cost obeying that law is forced to unit weight. In particular the power family $C_n$ and oscillatory family $C_{\mathrm{osc}}$ either fail the law or collapse to the same unit-weight $J$, so they cannot reparametrize away the constraint-sector kinetic normalization.

background

Gap 5 sits in the SevenGaps gravity campaign. Upstream, HKTKineticFromRecognitionCost (Pillar 1 work item 1) halves a disclosed constraint premise: the normalized kinetic momentum relation is of the form $S.hp,a,b,p=(2,c_{\mathrm{Kin}}),p$ with $c_{\mathrm{Kin}}\neq 0$ constant, and kill theorems there show rigidity fails if that premise is dropped. The remaining freedom is chart weight and reparametrization of the cost that feeds the kinetic term.

Recognition Science fixes the cost by the composition law (RCL), the functional equation whose unique nonnegative solution on $\mathbb{R}_{>0}$ is $J(x)=\cosh(\log x)-1$ (forcing chain T5). This module stays on the FunctionalEquation import path: it proves $J$ satisfies RCL via the repo's cosh-addition identity rather than importing full cost-uniqueness.

Sibling objects introduce candidate reparams: power costs $C_n$ and oscillatory costs. The attack is to show that RCL plus mild positivity forces unit weight, so those families cannot supply a genuine alternative normalization inside the constraint sector.

proof idea

Structure is lemma stack, not a single theorem. First, $J$ is shown to satisfy RCL by routing through the cosh-addition identity (keeps imports off CostUniqueness). Next, a generic lemma: any cost satisfying the composition law is forced to unit weight; the $J$ case is recorded as an instance. Power costs are defined, checked at $n=1$, shown to satisfy RCL when they do, and compared to $J$ (e.g. the $n=2$ power cost is not $J$). Positivity of $J$ on $(1,\infty)$ feeds the forcing. Oscillatory costs get the same RCL check. Net: every RCL-satisfying reparam collapses to unit weight, blocking escape from the canonical kinetic normalization.

why it matters in Recognition Science

The module is the reparametrization half of Gap 5's attack on residual freedom in the constraint sector. Downstream, Gap5O6ChartInvariant (Campaign 2 Track C) asks for the first parameter-free number the sector can produce: upstream already gives $c_{\mathrm{Kin}}=2\lambda^2>0$ with chart constant $\lambda$ free, and $2\lambda^2$ absorbs $\lambda$. O6 asks whether the ratio of kinetic to gradient coefficient in ADM form is chart-independent. That ratio is only meaningful once reparams that preserve RCL cannot change the weight; this module supplies that lock. In the broader framework it is local enforcement of T5 J-uniqueness and RCL inside gravity, before chart-invariant numerics.

scope and limits

Does not prove full global uniqueness of J; only RCL satisfaction via cosh-addition and unit-weight forcing for listed reparams.
Does not fix the chart constant λ or evaluate the O6 kinetic-to-gradient ratio.
Does not discharge the disclosed kinetic premise of HKTKineticFromRecognitionCost; it only blocks cost reparam escape.
Does not treat costs outside the power and oscillatory families introduced as siblings.
Does not import or replay CostUniqueness; stays on the FunctionalEquation path.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.Gap5O6ChartInvariant module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost module_import

declarations in this module (29)

theorem jcost_rcl L119
theorem compositionLaw_forces_unit_weight_generic L133
theorem compositionLaw_forces_unit_weight_is_an_instance L153
theorem satisfiesCompositionLaw_comp_pow L166
def powCost L177
theorem powCost_one L179
theorem powCost_satisfiesCompositionLaw L183
theorem powCost_two_ne_Jcost L189
theorem Jcost_pos_of_one_lt L196
theorem powCost_forces_unit_weight L206
def oscCost L242
theorem oscCost_satisfiesCompositionLaw L247
theorem oscCost_neg_at_exp_pi L258
theorem oscCost_forces_unit_weight L264
theorem oscCost_not_quadratic_in_log_chart L277
theorem G_powCost L296
theorem deriv2_G_powCost L302
theorem isCalibrated_powCost_iff L324
def CalibratedWeightAtTwo L341
theorem calibratedWeightAtTwo_forces_one L345
theorem rclWeight_zero L352
theorem not_calibratedWeightAtTwo_zero L358
theorem calibratedWeightAtTwo_ne_rclWeight L365
theorem falsifier_as_printed_is_met L383
theorem chart_alone_forces_the_cost L428
theorem Jlog_is_the_C_two_solution L447
theorem profile_clause_solution_set_is_a_scale_family L457
def constraint_sector_recognition_load_is_quadraticity_not_unit_weight L501
theorem constraint_sector_recognition_load_is_quadraticity_not_unit_weight_holds L512