Skip to content

Commit bcd2b85

Browse files
shuanatshuanat
committed
Add semantic hardening plan
1 parent 5a15864 commit bcd2b85

1 file changed

Lines changed: 137 additions & 0 deletions

File tree

‎SEMANTIC_HARDENING_PLAN.md‎

Lines changed: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
1+
# Semantic Hardening Plan (D.1 -> I.1)
2+
3+
## Goal
4+
5+
Replace compile-safe placeholders with mathematically meaningful Lean proofs across the production chain:
6+
7+
- no `axiom`
8+
- no `sorry`
9+
- no proxy theorem statements of the form `: True`
10+
11+
## Scope
12+
13+
Production proof chain files:
14+
15+
- `Collatz/Foundations/Core.lean`
16+
- `Collatz/Epochs/Core.lean`
17+
- `Collatz/Epochs/APStructure.lean`
18+
- `Collatz/Epochs/Homogenization.lean`
19+
- `Collatz/Epochs/NumeratorCarry.lean`
20+
- `Collatz/Epochs/LongEpochs.lean`
21+
- `Collatz/SEDT/Core.lean`
22+
- `Collatz/SEDT/Theorems.lean`
23+
- `Collatz/Mixing/Semigroup.lean`
24+
- `Collatz/Mixing/PhaseMixing.lean`
25+
- `Collatz/Mixing/TouchFrequency.lean`
26+
- `Collatz/CycleExclusion/CycleDefinition.lean`
27+
- `Collatz/CycleExclusion/PeriodSum.lean`
28+
- `Collatz/CycleExclusion/PureE1Cycles.lean`
29+
- `Collatz/CycleExclusion/MixedCycles.lean`
30+
- `Collatz/CycleExclusion/RepeatTrick.lean`
31+
- `Collatz/CycleExclusion/Main.lean`
32+
- `Collatz/Convergence/Coercivity.lean`
33+
- `Collatz/Convergence/FixedPoints.lean`
34+
- `Collatz/Convergence/NoAttractors.lean`
35+
- `Collatz/Convergence/MainTheorem.lean`
36+
37+
## Workstreams
38+
39+
### W1. Foundations Hardening
40+
41+
Target:
42+
43+
- Replace proxy definitions (`OddPred`, simplified `collatz_step`, etc.) with canonical forms.
44+
- Prove foundational arithmetic and parity lemmas needed by all downstream modules.
45+
46+
Done criteria:
47+
48+
- Core definitions match paper-level intent.
49+
- No theorem/lemma in this file uses `: True`.
50+
- Downstream files can import these lemmas without introducing local stubs.
51+
52+
### W2. Epoch Semantics (D.1 + G.5 prerequisites)
53+
54+
Target:
55+
56+
- Replace synthetic epoch quantities (`p_touch`, `long_epoch_density`, etc.) with derivable definitions.
57+
- Formalize AP structure, homogenization, and numerator carry lemmas with exact hypotheses.
58+
59+
Done criteria:
60+
61+
- D-level lemmas are real statements with executable hypotheses/conclusions.
62+
- Long-epoch machinery has a mathematically interpretable statement that can feed SEDT/mixing.
63+
64+
### W3. SEDT Core (E.2)
65+
66+
Target:
67+
68+
- Remove proxy numeric constants and bind them to explicit assumptions/derived bounds.
69+
- Replace placeholder bounds and witness-only proofs with inequalities used in subsequent modules.
70+
71+
Done criteria:
72+
73+
- `SEDT/Core` and `SEDT/Theorems` expose theorem statements that correspond to paper E.2 objects.
74+
- No placeholder existential witnesses (`⟨-1, by norm_num⟩` style) remain unless mathematically intended.
75+
76+
### W4. Mixing Layer (F.6/F.7)
77+
78+
Target:
79+
80+
- Formalize semigroup and phase-mixing statements as actual measure/frequency bounds.
81+
- Connect touch-frequency and mixing conclusions to SEDT inputs.
82+
83+
Done criteria:
84+
85+
- F.6/F.7 equivalent statements are explicit and consumed by H-level modules.
86+
- No vacuous proofs.
87+
88+
### W5. Cycle Exclusion (H.main)
89+
90+
Target:
91+
92+
- Replace `False`-based proxy predicates for cycle properties with real definitions.
93+
- Prove exclusion via period-sum and repeat-trick arguments over those real predicates.
94+
95+
Done criteria:
96+
97+
- `Cycle.is_pure_e1`, `Cycle.is_nontrivial`, and related notions are semantically meaningful.
98+
- `Main.lean` excludes nontrivial cycles from proven premises, not from definitional falsity.
99+
100+
### W6. Convergence Closure (I.1)
101+
102+
Target:
103+
104+
- Strengthen coercivity/fixed-point/no-attractor modules to formal implications.
105+
- Derive global convergence theorem from hardened D/E/F/G/H stack.
106+
107+
Done criteria:
108+
109+
- `Convergence/MainTheorem.lean` theorem statement corresponds to I.1 and depends only on proven lemmas.
110+
111+
### W7. CI and Acceptance
112+
113+
Target:
114+
115+
- Keep existing no-`sorry`/no-`axiom` gate.
116+
- Add semantic gate that rejects vacuous theorem signatures in production chain.
117+
118+
Done criteria:
119+
120+
- CI fails on new `: True` theorem declarations in production files.
121+
- `lake build Collatz` passes in CI and locally.
122+
123+
## Execution Order
124+
125+
1. W1 Foundations
126+
2. W2 Epoch semantics
127+
3. W3 SEDT core
128+
4. W4 Mixing
129+
5. W5 Cycle exclusion
130+
6. W6 Convergence
131+
7. W7 CI hardening
132+
133+
## Risk Notes
134+
135+
- Tight coupling between W2, W3, and W4 can cause theorem churn; stabilize interfaces early.
136+
- Avoid introducing new broad axiomatizations; prefer local assumptions and explicit parameter records.
137+
- Keep theorem names stable where possible to reduce cross-file rewrite overhead.

0 commit comments

Comments
 (0)