ledger_fraction_kn_forced_under_passive_bound_no_hk
plain-language theorem explainer
The theorem forces k exactly 4 and n exactly 0 whenever the normalized ledger fraction matches its canonical value under the passive-edge bound n ≤ E_passive. Mass-layer calculations in the Recognition framework cite it to close zeroth-order geometric shifts in the J-cost perturbation without a separate positivity hypothesis on k. The proof derives a contradiction for k = 0 from the explicit nonzero ledger fraction 29/44, then reduces directly to the positivity-assuming predecessor lemma.
Claim. If $n ≤ E_{passive}$ and $((W + E_{total} + n) / (k · E_{passive})) = $ ledger fraction, then $k = 4$ and $n = 0$.
background
The Mass-Layer J-Cost Perturbation module supplies the O4 perturbative closure for lepton-step masses. E_passive is the passive edge count, defined as passive_field_edges D and equal to 11. W and E_total are the base weights from the Anchor module; ledger_fraction is the fixed rational 29/44 supplied by the sibling lemma ledger_fraction_eq_29_over_44. The local setting certifies the J-cost(1+α) channel form together with the explicit α² + 12α³ radiative decomposition used in refined_shift.
proof idea
The tactic proof first performs case analysis on k = 0. The zero case produces the fraction equal to zero, which contradicts ledger_fraction_eq_29_over_44 (29/44 ≠ 0). With k > 0 established, the proof applies the predecessor theorem ledger_fraction_kn_forced_under_passive_bound to obtain the required pair k = 4 ∧ n = 0.
why it matters
This supplies the positivity-free integer closure that the downstream theorem base_shift_kn_forced_under_passive_bound_no_hk depends on for its packaged base_shift result. It completes the geometric forcing step inside the JCostPerturbation module for the refined shift. In the broader framework it constrains the phi-ladder rung parameters that feed the eight-tick octave and the D = 3 spatial dimensions without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.