How We Used Lean 4 to Formally Select an AI Logistics Implementation Site — Why Hiroshima Remained After Eliminating Bias
- kanna qed
- 3 時間前
- 読了時間: 5分
Introduction
We recently published a press release announcing a joint patent filing between On The Links Co., Ltd. and GhostDrift Mathematical Research Institute.
The centerpiece of that announcement is the joint patent — a system for recording and verifying AI logistics decisions in a form that companies can formally adopt with accountability.
But there was another major contribution from GhostDrift's side.
Formally demonstrating why Hiroshima.
For the selection of our implementation site, GhostDrift published a Lean 4 formalization on GitHub.
This article explains what is inside that formalization: why we chose to formalize, what we proved, and why Hiroshima remained after we worked to eliminate bias from the selection process as much as possible.
Why We Formalized
When selecting an implementation site for AI logistics, decisions are typically made based on existing relationships, the location of existing operations, or simply which conversations happened to move forward. None of that is inherently wrong, but from the outside it looks arbitrary.
That was exactly what we wanted to avoid.
We had a vision from the beginning: build an AI logistics assurance foundation starting from Hiroshima. But we wanted to present that not as "Hiroshima was always the plan" but as "we fixed the conditions first, ran the comparison, and Hiroshima came out."
The process we followed was:
Fix the evaluation criteria from international standards before looking at any city
Survey all ten major Japanese urban port regions against the same criteria
Formalize the results and publish them on GitHub
We chose Lean 4 because we wanted to publish in a form anyone can verify. This is not a claim from a single company — it is code, it is public, and the Lean type checker passes on GitHub Actions. If you disagree, you can disagree with the code.
How We Designed the Evaluation Criteria
We structured the criteria in two layers.
Layer 1: Screening Conditions (Physical and Infrastructure)
These are the minimum requirements for an AI logistics assurance testbed. We derived them from four international standards: ASAM OpenODD, EU AI Act, NIST AI RMF, and ISO 42001.
Port and logistics infrastructure exists
A manufacturing supply chain anchor connects continuously to the port
Urban human flow intersects the corridor (for human oversight design verification)
An ODD (Operational Design Domain) can be carved out
Logging points exist along the corridor
A human intervention path can be designed
The responsibility corridor is already closed without additional design work
The urban scale is not too large for an initial controlled experiment
The second-to-last condition deserves attention. "Closed responsibility corridor" is defined in Lean as ClosedODDCorridor using def rather than opaque. This was intentional: by defining it as the conjunction of four sub-predicates, the basis for "closed" becomes auditable rather than a black box.
Those four sub-predicates are:
HasBoundaryDefinition: the corridor boundary can be described
HasLoggingPoints: logging points exist
HasInterventionPath: a human intervention path can be designed
HasResponsibleActorsEnumerated: all responsible actors can be enumerated
We also required that the corridor be currently closed, not merely closable with additional design work. This was a pre-registered design decision made before surveying any city. We did not change it after seeing the results.
Layer 2: Institutional Integration Conditions (Governance)
These conditions ask whether a city that passes the physical screening can also support AI logistics assurance demonstration through its institutional structures. In Lean, this is defined as FullInstitutionalSandboxMatch.
An institutionally focused AI logistics assurance demonstration program exists
A mechanism for matching AI developers with local challenges exists
A public inventory of problems is maintained
In-region demonstration is required as an institutional condition
Public implementation support exists
A cross-administrative coordination layer exists
Results Across the Ten Cities
We surveyed the following ten major urban port regions in Japan using the same survey template: Tokyo, Osaka, Yokohama-Kawasaki, Nagoya, Fukuoka-Kitakyushu, Kobe, Sendai, Niigata, Hiroshima, and Okayama.
Screening condition results
Tokyo, Osaka, Yokohama-Kawasaki: Urban scale too large to establish a bounded initial ODD corridor (TooLargeForODDClosure)
Nagoya: Main container terminal is in Tobishima Village, spanning multiple municipalities (OverComplexForInitialODD)
Fukuoka-Kitakyushu: Two separate port authorities across two major cities make responsibility corridor design complex (OverComplexForInitialODD)
Kobe, Sendai, Niigata: Additional design work required before the corridor can be closed (CorridorRequiresDesignWork)
Hiroshima and Okayama: Passed
Institutional integration condition results
Okayama: Programs like GovTech Challenge OKAYAMA exist, but no AI logistics assurance-specific institutional focus was confirmed in primary sources
All other eight cities: First condition unconfirmed in primary sources
Hiroshima only: Passed
The Hiroshima AI Sandbox satisfied all six conditions: AI-specific focus, developer matching, public problem inventory, in-region demonstration requirement, public subsidies up to 100 million yen, and a cross-administrative coordination layer.
What We Proved in Lean
We formalized the survey results as three theorems in Lean 4.
Theorem 1: screening_narrows_to_two
theorem screening_narrows_to_two :
∀ c : SurveyCity, PassesScreen c →
c = SurveyCity.Hiroshima ∨ c = SurveyCity.Okayama
Only Hiroshima and Okayama satisfy the screening conditions. The proof exhausts all ten cities by case analysis.
Theorem 2: hiroshima_unique_full_institutional_sandbox
theorem hiroshima_unique_full_institutional_sandbox :
∀ c : SurveyCity, FullInstitutionalSandboxMatch c →
c = SurveyCity.Hiroshima
Only Hiroshima satisfies the institutional integration conditions.
One thing to be transparent about here: FullInstitutionalSandboxMatch is a conjunction of six conditions, but the proof of this theorem eliminates each city using only the negation of the first condition (HasAISpecificFocus). Whether the remaining five conditions are absent in each city is not formally verified in the Lean code.
This is an intentional design choice. A conjunction is false if any one conjunct is false, so the logic is correct. The verification of the remaining five conditions is delegated to the EvidenceReport, and a comment in the code explicitly states this.
Theorem 3: hiroshima_uniquely_satisfies_all_conditions
theorem hiroshima_uniquely_satisfies_all_conditions :
∀ c : SurveyCity,
PassesScreen c →
FullInstitutionalSandboxMatch c →
c = SurveyCity.Hiroshima
Only Hiroshima satisfies both conditions simultaneously. The proof actually calls Theorem 1 and Theorem 2. Theorem 1 narrows the candidates to Hiroshima and Okayama; Theorem 2 eliminates Okayama on institutional grounds. This two-stage structure is explicit in the proof term.
All three theorems are verified by the Lean type checker on GitHub Actions and currently pass CI.
What the Formalization Means and Where It Stops
This formalization proves that "if you accept these axioms, the theorems follow." It does not prove that the axioms themselves are correct.
For example, hiroshima_ai_specific — the axiom that Hiroshima has an AI-specific institutional focus — is grounded in primary sources from the Hiroshima AI Sandbox. Those sources are documented in the EvidenceReport. Whether the axiom correctly reflects those sources is a judgment that humans must make.
The value of the formalization is not that we "proved" anything in the colloquial sense. The value is that we made every assumption visible. Anyone who disagrees can point to a specific axiom and argue against it. That is what transparency looks like in formal terms.
Hiroshima Remained After Eliminating Bias
We had a vision of building from Hiroshima before we ran the survey. We fixed the criteria and ran the comparison anyway — not just to deflect the criticism of arbitrariness, but to verify our own judgment against a standard we set before looking at the data.
Hiroshima came out. That does not prove the vision was correct. But it does mean that "we checked with criteria we fixed in advance, and it still came out that way." That is the basis on which we proceed with confidence.
What Comes Next
This formalization is a starting point, not an endpoint.
HasClosedResponsibilityCorridor (field-level responsibility corridor design) and SupportsAssuranceLoggingExperiment (assurance logging infrastructure) remain unimplemented. An OpenODD format file for the Hiroshima corridor has not yet been created.
The next step is implementation. We will integrate the Logistics Decision Packet System into YUKAI and operate it across the Hiroshima port, manufacturing, and urban flow corridor. This work will connect to the establishment of the Hiroshima AI Assurance Council.
GhostDrift Mathematical Research Institute https://www.ghostdriftresearch.com
コメント