module module moderate

`IndisputableMonolith.Constants.PlanckScaleMatching`

The module PlanckScaleMatching introduces the J-cost functional to support Planck scale matching in Recognition Science. It supplies the definition J(x) = ½(x + x^{-1}) - 1 used in constant derivations. Researchers working on RS-native units for hbar and G cite this module. The module builds definitions from imported Cost and PhiForcing modules without internal proofs.

claim$J(x) = \frac{1}{2}(x + x^{-1}) - 1$

background

This module belongs to the Constants domain. It imports the base Constants module setting the RS time quantum τ₀ = 1 tick, the Cost module, and the PhiForcing module. As stated in the PhiForcing documentation: 'This module proves that φ is forced by self-similarity in a discrete ledger with J-cost.'

The module introduces the canonical cost functional J(x) = ½(x + x^{-1}) - 1, which underpins the Recognition Composition Law and J-related identities listed among its sibling definitions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds Planck scale matching and supplies the J definition required for constant derivations such as hbar = φ^{-5} and G = φ^5 / π. It supports the T5 J-uniqueness landmark in the forcing chain. No specific parent theorems appear in the used_by list.

scope and limits

Does not derive the forcing chain steps T0 to T8.
Does not prove the Recognition Composition Law.
Does not match the fine structure constant to its observed band.
Does not address the eight-tick octave or D = 3.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (35)

def J L45
theorem J_eq_Jcost L48
theorem J_exp_eq_cosh L51
def J_bit_val L60
theorem J_bit_eq_cosh L63
theorem J_bit_pos L71
theorem J_bit_explicit L80
theorem J_bit_eq_phi_minus L88
theorem J_bit_bounds L102
def cube_faces L113
theorem Q3_faces L116
def cube_vertices L119
theorem Q3_vertices L122
def J_curv L132
theorem J_curv_zero L135
theorem J_curv_nonneg L138
def lambda_rec_from_Jbit L148
theorem lambda_rec_from_Jbit_pos L151
theorem extremum_condition L156
theorem extremum_unique L163
def solid_angle_per_octant L175
def num_octants L178
def total_solid_angle L181
theorem octants_cover_sphere L184
def ell_P L192
theorem ell_P_pos L195
def lambda_rec_SI L208
theorem lambda_rec_SI_pos L211
theorem lambda_rec_over_ell_P L223
theorem one_over_sqrt_pi_approx L241
theorem planck_gate_identity L251
theorem planck_gate_normalized L260
structure PlanckScaleMatchingCert L287
def planck_scale_matching_cert L298
def planck_scale_matching_report L305