jCost_before_arithmetic
plain-language theorem explainer
The theorem places the J-cost stage before the arithmetic-object stage in the pre-temporal forcing order. Researchers building the dependency chain from recognition to time would cite this placement to maintain the sequence of prior structures. The proof succeeds via a one-line decide tactic that invokes the decidable instance on natural-number ranks.
Claim. In the pre-temporal forcing order, the stage for the J-cost proxy precedes the stage for arithmetic objects: $rank(J-cost) < rank(arithmeticObject)$.
background
The module records forcing priorities among stages that must exist before physical time is introduced. Stage is the inductive enumeration of these priorities: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. Before a b is defined as rank a < rank b and carries a Decidable instance via Nat.decLt. The module documentation states that A is before B precisely when B requires A as prior structure. The jCost stage imports the J-cost proxy from Decision.Trolley, which maps a TrolleyChoice to the real number of lives lost.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This succeeds because the Decidable instance for Before reduces the claim directly to a Nat.lt comparison on the ranks assigned to the two stages.
why it matters
The result continues the explicit ordering sequence that runs from rcl_before_jCost through jCost_before_arithmetic to arithmetic_before_time. It ensures the J-cost proxy is available before arithmetic objects appear, preserving the separation between recognition-light and physical light described in the module documentation. Within the Recognition Science framework this step belongs to the pre-temporal portion of the forcing chain that ultimately yields time ticks and three-dimensional space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.