jCost_before_arithmetic
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not define or compute the numerical ranks of any stage.
- Does not address the internal structure of arithmetic objects.
- Does not claim the order extends beyond the listed stages.
- Does not interpret the stages in physical spacetime.
formal statement (Lean)
93theorem jCost_before_arithmetic :
94 Before Stage.jCost Stage.arithmeticObject := by
proof body
Decided by rfl or decide.
95 decide
96