def
definition
xorBool
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
29 · have h' : q ≠ p := by intro hq; exact h hq.symm
30 simp [boolCost, h, h']
31
32def xorBool (p q : Bool) : Bool :=
33 xor p q
34
35/-- Strict discrete Boolean realization. -/
36def strictBooleanRealization : StrictLogicRealization where
37 Carrier := Bool
38 Cost := Nat
39 zeroCost := inferInstance
40 compare := boolCost
41 compose := xorBool
42 one := false
43 generator := true
44 identity_law := boolCost_self
45 non_contradiction_law := boolCost_symm
46 excluded_middle_law := True
47 composition_law := True
48 invariance_law := True
49 nontrivial_law := by
50 simp [boolCost]
51
52/-- Strict Boolean forced arithmetic is canonically `LogicNat`. -/
53def strictBoolean_arith_equiv_logicNat :
54 (StrictLogicRealization.arith strictBooleanRealization).peano.carrier
55 ≃ ArithmeticFromLogic.LogicNat :=
56 (StrictLogicRealization.toLightweight strictBooleanRealization).orbitEquivLogicNat
57
58/-- First strict cross-realization invariance theorem:
59positive ratios and Boolean propositions force the same arithmetic. -/
60noncomputable def strictPositiveRatio_arith_equiv_strictBoolean
61 (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
62 (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h)).peano.carrier