A2
plain-language theorem explainer
A2 supplies the explicit scaling form A2(P, γ) = P * phi^(-2γ) used to instantiate the multiplicative consistency axiom in Recognition Science derivations. Researchers working on DAlembert inevitability and bilinear family uniqueness cite it to fix the RCL polynomial scale. The definition is a direct abbreviation that substitutes the golden-ratio fixed point into the exponent.
Claim. $A_2(P, γ) := P φ^{-2γ}$ where $φ$ denotes the self-similar fixed point of the Recognition Composition Law.
background
In the VoxelWalks module, A2 appears among the core scaling abbreviations that support voxel-walk cost calculations. It rests on the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and the normalization J(1) = 0. Upstream, RCL_unique_polynomial_form records that compatibility constraints plus continuity and non-constancy force a unique bilinear family via Aczél's functional-equation theory.
proof idea
One-line abbreviation that directly applies real exponentiation to the imported phi constant; no lemmas or tactics are invoked.
why it matters
A2 instantiates the A2 (RCL) slot inside axiom_bundle_necessary, which concludes that the full axiom bundle is transcendentally necessary, and inside bilinear_family_forced, which derives the unique bilinear family. It therefore anchors the T5 J-uniqueness and T6 phi-fixed-point steps of the forcing chain and is referenced by downstream results on monotonicity, local cache costs, and brain-holography inevitability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.