theorem proved term proof

`plot_count_scaling`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 245theorem plot_count_scaling (D : ℕ) :
 246    (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card = 2 ^ D - 1 :=

proof body

Term-mode proof.

 247  F2Power.nonzero_card
 248
 249/-! ## §5. Weight decomposition matches Booker's primary/compound/transcendent -/
 250
 251/-- The Hamming weight of a Booker plot's encoding equals the number
 252    of narrative axes the plot transforms. -/

depends on (7)

Lean names referenced from this declaration's body.

F2Power in IndisputableMonolith.Algebra.F2Power decl_use
nonzero_card in IndisputableMonolith.Algebra.F2Power decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use