| /- | |
| Sovereign Apollo — State + MET + Guidance Mode | |
| Evidence: TIMELINE-001, ERASABLE_ASSIGNMENTS, LUM099-001 | |
| -/ | |
| inductive GuidanceMode where | |
| | IU | P00 | P12 | P20 | P30 | P40 | P63 | P64 | P66 | P68 | IDLE | |
| deriving DecidableEq, Repr | |
| inductive VehicleState where | |
| | StackThrusting | LEO | TLI | Coast | LunarOrbit | PDI | Surface | Ascent | Docked | TEI | Reentry | |
| deriving DecidableEq, Repr | |
| structure State where | |
| metSeconds : Nat | |
| vehicle : VehicleState | |
| guidance : GuidanceMode | |
| massKg : Nat | |
| dryMassKg : Nat | |
| throttlePermille : Nat -- 0..1000 (100 = 10%) | |
| deriving Repr | |
| def State.throttleOk (s : State) : Prop := | |
| (s.guidance = .P63 ∨ s.guidance = .P64) → | |
| (100 ≤ s.throttlePermille ∧ s.throttlePermille ≤ 940) | |
| theorem fuel_nonnegative (s : State) (h : s.massKg ≥ s.dryMassKg) : s.massKg ≥ s.dryMassKg := h | |