discreteRealization
plain-language theorem explainer
The definition supplies the Boolean carrier as the discrete realization of the Law-of-Logic structure. Researchers working on the universal forcing chain cite it when establishing equivalence between continuous and discrete arithmetic models. It is realized as a direct alias to the boolRealization definition.
Claim. The discrete realization is the Boolean propositional realization of the Law-of-Logic structure, with carrier set $Bool$, cost type $Nat$, comparison function $boolCost$, and zero element $false$.
background
The LogicRealization structure consists of a carrier type, a cost type equipped with zero, a compare function between carriers, and a distinguished zero element; these fields supply the structural laws needed by the Universal Forcing program. The boolRealization definition populates this structure with the Boolean type as carrier and natural numbers as costs, yielding the discrete propositional case. The present module re-exports that construction under the UniversalForcing tree so that arithmetic extraction can reference a canonical discrete model.
proof idea
The definition is a one-line wrapper that directly returns boolRealization.
why it matters
This supplies the discrete side for the arithmetic equivalence theorems, including discrete_arith_equiv_logicNat and arith_continuous_equiv_arith_discrete. It anchors the Boolean case in the forcing chain, enabling extraction of Peano arithmetic from the discrete realization and supporting the canonical equivalence between continuous positive-ratio arithmetic and discrete Boolean arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.