module module moderate

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostStructuralLedger`

Structural ledger for the primitive recognition native cost: a cross-equivalence of displays is treated as equality of those displays, and a real character cost jq is recorded with its orbit, closed-form, and sign properties. Cost and gauge-orbit work cites this layer when the J-cost must sit on ratio orbits rather than abstract certificates. The module is definitional bookkeeping plus elementary algebraic identities, not a deep existence proof.

claimA cross-equivalence of displays is identified with equality of the corresponding display values. On that ledger one records a real character cost $j_q$ on ratio orbits, with $j_q(1)=0$, closed form, nonnegativity, and the usual zero/negative sign rules, together with the identification of the character cost with $j_q$.

background

Primitive Recognition Calculus (PRC) builds the native cost before the full forcing chain is invoked. Upstream sits the native-cost minimality certificate module, which supplies the certificate that the cost is minimal among admissible recognition functionals. Here the ledger is structural: displays and their cross-relations are the raw data, and a cross-equivalence is read simply as equality of displays rather than as a separate quotient construction.

The main object introduced is the real character cost $j_q$ (siblings: orbit restriction, cost-from-character identification, and the elementary facts $j_q(1)=0$, closed form, nonnegativity, and sign/zero rules). In Recognition Science this is the same family as the T5 J-cost $J(x)=(x+x^{-1})/2-1$, specialized to the character/ratio-orbit setting used by the native cost. The module therefore sits between abstract minimality and concrete gauge-orbit calculus.

proof idea

Definition module with elementary algebraic lemmas, not a single deep theorem. Cross-display equivalence is packaged as display equality; $j_q$ is defined (or identified) on ratio orbits and tied to the character cost. The remaining declarations are short facts: value at one, closed form, nonnegativity, and the zero/negative cases. Expect direct unfolding, rewriting along the orbit, and standard real inequalities rather than a multi-step forcing argument.

why it matters in Recognition Science

Feeds the cost-side gauge-orbit development: Cost.GaugeOrbitFromRealCharacter imports this ledger so that gauge orbits can be read from a real character whose cost is already native and structurally normalized. Without the cross-display equality convention and the $j_q$ package, orbit arguments would still talk in certificates rather than in display equalities and explicit character costs.

In the broader framework this is bookkeeping under the Recognition Composition Law and T5 J-uniqueness: the same $J$-shape appears as $j_q$ on ratio orbits, ready for gauge and cost modules downstream. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only makes the native cost legible to those later steps.

scope and limits

Does not prove J-uniqueness (T5) or force the closed form from the RCL alone.
Does not derive phi, the eight-tick period, or D = 3.
Does not construct gauge orbits; that lives in the downstream cost module.
Does not replace the upstream minimality certificate; it only structures displays and jq.
Does not claim numerical constants (alpha band, mass ladder, G, hbar).

used by (1)

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

IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimalityCertificate module_import

declarations in this module (104)

theorem crossDisp L69
theorem dispCross L73
def jq L77
theorem jq_onRatioOrbit L79
theorem costFromCharacter_jq L82
theorem jq_one L85
theorem jq_zero L87
theorem jq_closed L89
theorem jq_nonneg L94
theorem jq_lt_zero L98
theorem jq_eq_zero L105
theorem jq_neg L116
theorem jq_inv L121
theorem jq_mono L128
theorem jq_strictMono L143
theorem jq_le_reflect L160
theorem jq_rcl L168
theorem jq_two L176
theorem jq_eq_two_cases L179
def natOrbit L199
theorem natOrbit_toRat L201
def IsPosIntOrbit L205
theorem natOrbit_isPosInt L207
theorem two_isPosInt L210
theorem primeDirection_isPosInt L212
def PRCNativeCostSignReversing L228
def PRCNativeCostMonotone L234
def PRCNativeCostPositive L240
theorem canonicalSelectedNativeCost_jq L245
theorem canonicalSelectedNativeCost_signReversing L249
theorem canonicalSelectedNativeCost_monotone L259
theorem canonicalSelectedNativeCost_positive L267
theorem signReversing_forces_signed_unit L277
structure PRCSignReversingNativeCostHypotheses L291
def PRCSignReversingNativeCostUniquenessTarget L297
theorem PRCSignReversingNativeCostUniquenessTarget_proved L303
theorem canonicalSelectedNativeCost_signReversing_hypotheses L316
theorem signReversing_class_forces_slim L326
theorem absValueGeneratedNativeCost_not_signReversing L339
lemma exists_pow_gt_rat L363
lemma cut_pins_aux L378
theorem cut_pins L414
structure MonoMult L428
theorem pow L436
theorem pos L445
theorem ge_one L461
theorem transfer_le L502
theorem transfer_ge L511
theorem trivial_of_two_eq_one L522
theorem monoMult_gauge L548
theorem natCast_monoMult L569
theorem monotone_multiplicative_pins L580
structure PRCStructuralNativeCostHypotheses L594
def PRCStructuralNativeCostUniquenessTarget L601
theorem structural_character_calibrated_on_positive_integers L609
theorem PRCStructuralNativeCostUniquenessTarget_proved L688
theorem canonicalSelectedNativeCost_structural_hypotheses L744
theorem structural_forces_slim L755
theorem structural_forces_positive L770
structure PRCStructuralNativeCostHypothesesSansAnchor L786
def PRCStructuralSansAnchorUniquenessTarget L793
theorem structural_iff_sansAnchor_and_two_calibrated L800
def powerGeneratedNativeCost L833
theorem powerGeneratedNativeCost_toRat L837
theorem powerGeneratedNativeCost_base L845
theorem powerGeneratedNativeCost_monotone L865
theorem powerGeneratedNativeCost_zero_calibrated L873
theorem powerGeneratedNativeCost_signReversing L884
def oddPowerGeneratedNativeCost L892
theorem oddPowerGeneratedNativeCost_toRat L895
theorem oddPowerGeneratedNativeCost_sansAnchor L899
theorem oddPowerGeneratedNativeCost_anchor_injective L911
def cubeGeneratedNativeCost L927
theorem cubeGeneratedNativeCost_toRat L930
theorem cubeGeneratedNativeCost_sansAnchor L934
theorem oddPowerGeneratedNativeCost_zero L940
theorem cubeGeneratedNativeCost_two_not_canonical L945
def GaugeOrbitIsOddPowerFamily L1065
theorem gauge_orbit_contains_every_odd_power L1072
theorem PRCStructuralSansAnchorUniquenessTarget_refuted L1083

… and 24 more