gap_balance
plain-language theorem explainer
The phi-power balance identity at D=3 shows that phi raised to (active-edge count minus integration gap) times phi to the gap power equals phi. Recognition Science researchers cite it when verifying exponent closure on the phi-ladder inside mass formulas. The proof is a short tactic sequence that substitutes the precomputed gap value 45, rewrites the active-edge count as 1, and reduces the combined exponent via zpow_add and norm_num.
Claim. $phi^{1-g}cdot phi^g=phi$ where the active edge count per tick equals 1 and the integration gap $g$ equals 45 at the forced spatial dimension 3.
background
The integration gap is defined as the product of parity count and configuration dimension for a given spatial dimension D. At D=3 this product equals 45. The active edge count per fundamental tick is fixed at 1. The module also establishes that gcd of 2^D with the gap equals 1 precisely when D is odd, which combines with the dimension-forcing argument to select D=3 among odd candidates.
proof idea
The tactic proof first obtains the integer value 45 for the gap at D=3 from the upstream result integrationGap_at_D3. It rewrites the active edge count as 1 and applies zpow_add₀ to combine the exponents. A norm_num step confirms that 1 minus 45 plus 45 equals 1, after which zpow_one produces the right-hand side phi.
why it matters
This identity supplies the required exponent cancellation for the phi-ladder when the integration gap appears in mass formulas. It sits inside the foundation layer that precedes the mass and actualization modules and is consistent with the eight-tick octave and D=3 selection from the forcing chain. No downstream theorems are listed, so the result functions as a local arithmetic closure check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.