def
definition
HitsBalancedPhaseLogic
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.LogicErdosStrausBoxPhase on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
48/-- Logic-native box-phase hit, transported to the current classical hit
49predicate. This keeps the finite phase proof surface stable while recording
50that the carrier is recovered from the Law of Logic. -/
51def HitsBalancedPhaseLogic (n c : LogicNat) : Prop :=
52 ErdosStrausBoxPhase.HitsBalancedPhase (toNat n) (toNat c)
53
54theorem hitsBalancedPhaseLogic_iff_classical (n c : LogicNat) :
55 HitsBalancedPhaseLogic n c ↔
56 ErdosStrausBoxPhase.HitsBalancedPhase (toNat n) (toNat c) :=
57 Iff.rfl
58
59/-- A recovered box-phase hit gives the logic-native rational
60Erdős-Straus representation. -/
61theorem box_phase_hit_gives_repr_logic {n c : LogicNat}
62 (h : HitsBalancedPhaseLogic n c) :
63 HasRationalErdosStrausReprLogic (fromRat (toNat n : ℚ)) := by
64 apply reprLogic_fromRat_of_classical
65 exact ErdosStrausBoxPhase.box_phase_hit_gives_repr h
66
67end LogicErdosStrausBoxPhase
68end NumberTheory
69end IndisputableMonolith