module module moderate

`IndisputableMonolith.Constants.PlanckScaleMatching`

This module assembles definitions for matching Planck-scale constants to the Recognition Science framework using the J-cost functional and phi-forcing. It composes the discrete ledger self-similarity result with the canonical cost J(x) to produce RS-native expressions for ħ, G and related scales. Physicists working on constant unification would cite it when deriving mass ladders or alpha-band values from the phi-ladder. The module itself contains no proofs and simply imports and re-exports the required objects from Constants, Cost and PhiForc

claimThe canonical cost functional satisfies $J(x)=½(x+x^{-1})-1$. Planck-scale constants are expressed in RS-native units by $c=1$, $ħ=ϕ^{-5}$, $G=ϕ^5/π$, with $α^{-1}$ lying in the interval $(137.030,137.039)$.

background

The module sits inside the Recognition Science derivation of physics from a single functional equation. It imports the fundamental RS time quantum τ₀=1 tick from Constants, the J-cost structure whose doc-comment states “The canonical cost functional J(x)=½(x+x^{-1})-1”, and the PhiForcing module whose argument shows that ϕ is forced by self-similarity in a discrete ledger equipped with J-cost. These three imported modules supply the J-cost, the phi-ladder and the eight-tick octave needed to express Planck quantities without additional hypotheses.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Planck-scale matching step required by the unified forcing chain (T0–T8) and by the mass formula yardstick·ϕ^(rung-8+gap(Z)). It therefore feeds directly into downstream derivations of particle masses and the fine-structure interval. Because used_by is empty at present, it functions as an interface that later theorems on Berry creation and dream-fraction thresholds will invoke.

scope and limits

Does not derive numerical values beyond the explicit ϕ expressions.
Does not incorporate loop corrections or higher-order phi-ladder terms.
Does not contain experimental data or fitting procedures.
Does not address non-RS units or conversion factors.

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