virtueCost_phi_step
plain-language theorem explainer
The theorem states that the J-cost of the golden ratio φ equals exactly φ minus 3/2. Researchers extending the Recognition Science ethics module cite it to fix the deviation cost of a single φ-step virtue generator. The result upgrades the pre-Big-Bang paper scaffold by supplying a concrete numerical anchor for the 14 DREAM generators. The proof is a direct one-line reference to the upstream lemma that evaluates Jcost at φ.
Claim. $Jcost(φ) = φ - 3/2$, where $Jcost$ is the J-cost function and $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module constructs virtue generators from J-cost to upgrade the SCAFFOLD tag in pre_big_bang_origin_paper.tex §virtues. It asserts a finite set of 14 canonical σ-preserving micro-moves (the DREAM generators) whose bidirectional structure spans the algebra of local σ-zero moves in F₂³, with cardinality fixed by the Count Law at D=3. J-cost is the deviation measure imported from the Cost module; φ is the self-similar fixed point from the forcing chain. The upstream lemma Jcost_phi_val states: “J(φ) = φ - 3/2 (exact, using φ² = φ + 1).”
proof idea
The proof is a one-line term wrapper that directly applies the lemma Jcost_phi_val from IndisputableMonolith.Constants.
why it matters
This supplies the exact J-cost anchor for the φ-step inside the virtue-generator construction, feeding the structural claim that 14 generators span all σ-preserving moves. It advances the pre-Big-Bang paper upgrade from scaffold to partial theorem while leaving the completeness conjecture (C4) open. The value ≈0.118 quantifies the minimal deviation cost per generator in the RS-native units where c=1 and φ is the fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.