module module low

`IndisputableMonolith.Constants.PlanckScaleMatching`

Module PlanckScaleMatching defines the canonical cost functional J(x) = ½(x + x⁻¹) - 1 as the basis for Planck scale matching in Recognition Science. Researchers building constants from self-similar discrete ledgers would cite this definition. It imports the time quantum τ₀ from Constants and the self-similarity argument from PhiForcing to ground the J-cost structure.

claimThe canonical cost functional is given by $J(x) = ½(x + x^{-1}) - 1$.

background

The module sits in the Constants domain. It imports the fundamental RS time quantum τ₀ = 1 tick. The Cost module supplies the J-cost structure. PhiForcing proves that φ is forced by self-similarity in a discrete ledger with J-cost, quoting its documentation: 'This module proves that φ is forced by self-similarity in a discrete ledger with J-cost.'

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the J functional that supports Planck scale matching and constant derivations from the phi-ladder. It connects directly to the PhiForcing result on self-similarity. No direct downstream uses appear in the module graph.

scope and limits

Does not prove any theorems or matching results.
Does not contain numerical comparisons to observed constants.
Does not define the phi-ladder or rung structure.
Does not extend the forcing chain T0-T8.

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