module module moderate

`IndisputableMonolith.Constants.LambdaRecDerivation`

LambdaRecDerivation module derives the recursive lambda as the unique positive root of the balance residual equation built from the normalized bit cost of a recognition event. Researchers establishing RS-native constants or the phi-ladder would cite it for the lambda_0 and root-uniqueness results. The module consists of supporting definitions for totalCost and balanceResidual followed by root-isomorphism and uniqueness statements.

claimLet $J_{bit}$ be the normalized bit cost of one recognition event. Define $ au_0 = 1$ tick as the base quantum. Then $\lambda_{rec}$ is the unique positive root of the balance residual equation, with $alanceResidual( au_0, otalCost, alanceAtLambda_0)$ vanishing only at this root.

background

The upstream Constants module defines the fundamental RS time quantum as $ au_0 = 1$ tick. This derivation submodule introduces $J_{bit}$ (normalized bit cost of one recognition event) together with totalCost, balanceResidual, lambda_0, and the auxiliary lemmas lambda_0_pos, lambda_0_sq, and balance_at_lambda_0. These objects sit inside the larger Constants framework that supplies the J-cost function and the Recognition Composition Law.

proof idea

This is a definition module, no proofs. It introduces the auxiliary quantities J_bit_normalized, totalCost, and balanceResidual, states lambda_rec_is_root, and records the uniqueness claim lambda_rec_unique_root.

why it matters in Recognition Science

The module supplies the recursive lambda root required by the parent Constants module for subsequent constant derivations. It fills the step that isolates the unique positive solution to the balance equation, directly supporting the phi-ladder mass formulas and the alpha-band predictions in the Recognition Science chain.

scope and limits

Does not supply numerical approximations to lambda_rec.
Does not connect the root to physical units or measurements.
Does not address extensions beyond the one-dimensional balance equation.
Does not prove existence outside the positive reals.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (26)

def J_bit_normalized L28
def J_curv L34
def totalCost L37
def balanceResidual L41
def lambda_0 L45
lemma lambda_0_pos L47
lemma lambda_0_sq L53
theorem balance_at_lambda_0 L61
theorem balance_unique_positive_root L67
def K L92
theorem lambda_rec_is_root L95
theorem lambda_rec_unique_root L100
theorem lambda_rec_is_forced L114
def Q3_vertices L144
def Q3_faces L147
def euler_S2 L150
def dihedral_angle L153
def angular_deficit_per_vertex L156
theorem angular_deficit_value L159
theorem total_curvature_gauss_bonnet L164
def kappa_normalized L169
theorem kappa_normalized_eq_one L172
theorem J_curv_derivation L182
theorem balance_determines_lambda L186
structure GDerivationChain L209
theorem G_derivation_chain_complete L217