lemma proved term proof

`twoSystems_length`

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

formal statement (Lean)

  49lemma twoSystems_length (n mask : Nat) :
  50    ([systemOfMask n mask false, systemOfMask n mask true] : List (XORSystem n)).length = 2 := rfl

proof body

Term-mode proof.

  51
  52/-- Linear family length bound: exactly 2 * (n+1)².
  53    Proof sketch: flatMap over range(k) where each element contributes list of length 2
  54    gives total length k * 2 = 2 * (n+1)². -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

linearFamily_length_eq in IndisputableMonolith.Complexity.SAT.SmallBias decl_use

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
systemOfMask in IndisputableMonolith.Complexity.SAT.SmallBias decl_use
XORSystem in IndisputableMonolith.Complexity.SAT.XOR 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
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use