log_phi_gauge_invariant
plain-language theorem explainer
The statement establishes that the natural logarithm of the self-similar fixed point phi equals itself for arbitrary nonzero real rescalings alpha and k. Researchers checking gauge invariance of dimensionless constants in Recognition Science reference this result when confirming that phi survives ledger rescalings unchanged. The argument reduces to introducing the four hypotheses and applying reflexivity.
Claim. For all nonzero real numbers $alpha$ and $k$, $log phi = log phi$.
background
The module distinguishes gauge freedom (rescalings p to alpha p plus b and J to k J) from physical parameters, showing that dimensionless outputs such as alpha inverse remain unique across choices. Phi enters as the fixed point forced by the self-similar condition in the unified forcing chain. The local setting treats log phi as an intermediate quantity whose invariance under gauge transformations supports later claims that alpha inverse is independent of unit conventions.
proof idea
The term proof introduces the four assumptions via intro and closes with rfl, confirming the identity holds identically.
why it matters
This invariance anchors the gauge-invariance arguments for alpha inverse and related quantities in the same module. It aligns with the framework landmark that phi is the self-similar fixed point (T6), ensuring log phi contributes a gauge-independent term to expressions such as alpha inverse equals 4 pi times 11 minus ln phi minus 103 over 102 pi to the fifth. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.