length_unaryEncode
plain-language theorem explainer
The unary Boolean list for a natural number n has list-length exactly n. Downstream exclusivity proofs cite it when decoding algorithmic codes via length, so that every natural (hence every enumerated state) recovers cleanly. The proof is a one-line simp that unfolds the replicate definition.
Claim. For every natural number $n$, if $\mathrm{unaryEncode}(n)$ is the Boolean list that repeats $\mathsf{true}$ exactly $n$ times, then the length of that list equals $n$.
background
This module supplies shared PhysicsFramework scaffolding for the NoAlternatives and necessity arguments, keeping core definitions free of circular imports.
Unary encoding is the local bridge from naturals into finite Boolean codes: $\mathrm{unaryEncode}(n) := \mathrm{List.replicate}, n, \mathsf{true}$. Algorithmic specifications in this file generate codes from naturals and decode by reading code length, so the length identity is the arithmetic hinge.
The name collision with Trace length in PrimitiveRecognitionCalculus is incidental; here length is ordinary List.length on Bool lists. Upstream, unaryEncode is the noncomputable replicate wrapper used by HasAlgorithmicSpec.ofEquivNat and ofNatSurjection.
proof idea
One-line tactic proof: simp unfolds unaryEncode to List.replicate n true. Mathlib's length_replicate (or the simp normal form of List.length on replicate) immediately yields length = n. Marked @[simp] so later exclusivity constructions discharge the same identity automatically.
why it matters
Exclusivity needs a zero-parameter witness: every framework state must arise from a finite algorithmic code with no free constants. Unary encoding plus this length identity lets HasAlgorithmicSpec.ofEquivNat and ofNatSurjection equip any type equivalent (or surjected) from ℕ with such a spec; those feed HasZeroParameters.ofLedgerEquiv when a ledger equivalence is present.
In the Recognition chain this is bookkeeping, not a forcing step (not T5–T8), but it closes the enumeration side of the "no free parameters" claim used by NoAlternatives. No downstream edges are recorded yet; the immediate consumers sit in the same Framework section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.