Established within the stated premises
Pascal condition has exactly the solution five for all natural g
finding:pascal-carrier-rank-unique-unbounded-source-proof
CarrierRankUniqueness.carrier_rank_pascal_unique states and proves for every natural g that 2^g=g^2+g+2 iff g=5. Its proof combines the small cases with pascal_growth for all g>=6. This is unbounded; PascalLadder has a separate bounded K=2 statement. For g=5, N_fam=3 and g+N_fam=8 are computed.
Scope: Algebraic uniqueness under the stipulated Pascal/half-spinor exhaustion condition. Original source and proof text reviewed; no fresh Lean kernel run. AX.P2.01 remains a declared physical interface; the equation does not select itself from an original source.
Required premises and original source excerpts
- Pascal exhaustion condition as input
g is natural; the stipulated equation is 2^g=g^2+g+2. The equation itself is the additional carrier exhaustion rule.
premise:pascal-carrier-exhaustion-equation
- experiments/lean4-carrier-rigidity/TfptCarrier/CarrierRankUniqueness.lean, lines 32–86
Source SHA256: b872e8ced3fc07b2e0af4a0acd7e107f4792a4a8006ed34a74f455f566de735b
bounded-excerpt · current-at-snapshot
- documents/tfpt_3_e8_audit_bootstrap/sections/013-section-honest-status-bootstrap-not-creation-from-nothin.tex, lines 316–345
Source SHA256: 80eea5c25d9ca99fd6bcee1676d334155e007c1f2cda7e797f7ec8a2713c23af
bounded-excerpt · current-at-snapshot