formalization.yaml

# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json
#
# formalization.yaml (Mathlib Initiative schema v0.4) for the Lean 4
# formalization backing the preprint "The Unique Ordinary Element of a
# One-Generated Heyting Algebra, the Subgroup Lattice of Z/12Z, and a
# Characterization of n = p^2 q" (preprints/ordinary-elements-z6/).
#
# The Lean project lives in lean/ (not the repository root): toolchain in
# lean/lean-toolchain, dependency pins in lean/lake-manifest.json, build in
# .github/workflows/comparator.yml. Those are not duplicated here.
#
# History: first written 2026-07-12 in a pre-v0.4 ad hoc shape; migrated to
# v0.4 on 2026-10-12. Keys outside the v0.4 template (verification,
# scope_files, known_gaps, additional_tracks) are retained as extra keys,
# which the schema permits.

version: "v0.4"

project:
  name: falsework-papers-ordinary-elements
  description: >-
    Kernel-checked structure theory of one-generated Heyting algebras:
    Nishimura's one-variable normal form, the four-region non-degeneracy
    criterion (all four regions relative to a are inhabited iff a is
    ordinary, i.e. neither regular nor dense), uniqueness of the ordinary
    element in an algebra one-generated by an ordinary element (statement
    in Citkin 2025, previously unproved), the six-element threshold and the
    Z6 order-embedding forced by any ordinary element, the H8 converse
    counterexample, the divisor lattice of 12 as Z6 with the divisor 2
    (tritone) as unique ordinary element, the p^2 q characterization and
    the general k-prime existence/uniqueness/count laws, and the
    substitution monoid End(Z6) = Z6.
  authors:
    - "Claude (Anthropic), AI, working in Cursor: all Lean proofs"
    - "Chris Brink: direction, statement review, prior-art adjudication"
  responsible_maintainers:
    - "Chris Brink (chris@falsework.dev)"
  license: "CC-BY-4.0 (preprint); Apache-2.0 (Lean sources, see LICENSE-CODE)"

repository:
  role: substantive-development

sources:
  - title: >-
      The Unique Ordinary Element of a One-Generated Heyting Algebra, the
      Subgroup Lattice of Z/12Z, and a Characterization of n = p^2 q
    authors: ["Chris Brink"]
    id: preprints/ordinary-elements-z6/paper.md
    type: preprint
    location: "Theorems 3.2, 4.1, 4.2, 5.1, 5.2, 8.1(4) (comparator scope); section 10 audit table"
    relationship: formalizes
    author_endorsement: participated
    note: >-
      Paper and formalization were developed together by the same author;
      the paper's section 10 is the per-theorem audit table of the Lean.
  - title: "Hereditarily structurally complete superintuitionistic logics and primitive varieties of Heyting algebras"
    authors: ["Alex Citkin"]
    id: "arXiv:2512.05633"
    type: article
    location: "p. 13: Z_n contains a single ordinary element that generates the entire algebra (asserted without proof)"
    relationship: formalizes
    author_endorsement: other
    note: >-
      The uniqueness statement (unique_ordinary_element) is Citkin's; the
      written proof here is apparently the first. Prior-art standing was
      adjudicated by correspondence with Citkin (personal communication
      2026-06-11, cited with permission; record at docs/outreach/citkin-email.md).
      That correspondence concerned novelty, not review of the Lean; it is
      not an endorsement of the formalization.
  - title: "An algebraic proof of the Nishimura theorem"
    authors: ["Alex Citkin"]
    id: "Logics 2(4), 2024, 148-157"
    type: article
    relationship: background
    author_endorsement: not-contacted
    note: >-
      Definitions of regular, dense, ordinary (section 2.1); Theorem 6
      (exactly one one-generated Heyting algebra of each finite cardinality)
      is used as a literature dependency for the identification Div12 = Z6
      in the paper's Theorem 7.1; Proposition 4(c) is the one-generated
      special case of the threshold theorem.
  - title: "On formulas of one variable in intuitionistic propositional calculus"
    authors: ["Iwao Nishimura"]
    id: "Journal of Symbolic Logic 25, 1960"
    type: article
    relationship: independently-proves
    author_endorsement: n/a
    note: >-
      nishimura_normal_form is the classical one-variable normal form; the
      Lean proof is the project's own (closure tables over the ladder), not
      a transcription of Nishimura's or Citkin's argument.
  - title: "A remark on the so-called free closure algebras"
    authors: ["Ladislav Rieger"]
    id: "Czechoslovak Mathematical Journal 7, 1957"
    type: article
    relationship: background
    author_endorsement: n/a

related_formalizations:
  - id: https://github.com/leanprover-community/mathlib4
    relationship: builds-on
    note: >-
      Pinned in lean/lake-manifest.json. The challenge module uses only
      Mathlib's HeytingAlgebra, OrderEmbedding, Fintype and Fin vocabulary.

classification:
  arxiv: ["math.LO"]
  msc2020: ["06D20", "03B55", "06D15"]

automation:
  methods:
    - method: agent
      models: ["Claude (Anthropic); per-file model versions not recorded"]
      framework: "Cursor"
      tool_setup: >-
        Interactive agent sessions in Cursor against the pinned Lean/Mathlib
        toolchain; lake build as the loop; #print axioms per theorem; a
        second, independent AI model used for a cross-model pre-audit of the
        challenge statements (2026-07-12).
      prompting_notes: >-
        Theorems were stated by the human author in prose, formalized by the
        agent, and iterated until kernel-accepted; the human author is not a
        Lean reader and reviewed statements, not proofs.
  spend_usd: "subscription-based usage"
  notes: >-
    All Lean in scope was AI-authored under human direction. Paper prose was
    drafted with AI assistance and edited by the human author.

status:
  scope: >-
    Complete for the paper's claims as listed in alignment below, with two
    stated exceptions (known_gaps). The comparator pair lean/Challenge.lean
    (Mathlib-only statements) and lean/Solution.lean covers six principal
    theorems; the remaining results in the audit table are kernel-checked in
    the library but not restated in the challenge module.
  sorry_count: 0
  sorry_in_definitions: 0
  axioms: ["propext", "Classical.choice", "Quot.sound"]
  main_results:
    - declaration: four_regions_iff_ordinary
      file: lean/FalseWorkPapers/Examples/ChallengeBridge.lean
      sorry_count: 0
      axioms: ["propext"]
      comparator_config: lean/config.json
    - declaration: nishimura_normal_form
      file: lean/FalseWorkPapers/Examples/ChallengeBridge.lean
      sorry_count: 0
      axioms: ["propext", "Quot.sound"]
      comparator_config: lean/config.json
    - declaration: unique_ordinary_element
      file: lean/FalseWorkPapers/Examples/ChallengeBridge.lean
      sorry_count: 0
      axioms: ["propext", "Quot.sound"]
      comparator_config: lean/config.json
    - declaration: ordinary_forces_card_ge_six
      file: lean/FalseWorkPapers/Examples/ChallengeBridge.lean
      sorry_count: 0
      axioms: ["propext", "Classical.choice", "Quot.sound"]
      comparator_config: lean/config.json
    - declaration: ordinary_gives_z6_embedding
      file: lean/FalseWorkPapers/Examples/ChallengeBridge.lean
      sorry_count: 0
      axioms: ["propext", "Classical.choice", "Quot.sound"]
      comparator_config: lean/config.json
    - declaration: twelve_unique_kernel
      file: lean/FalseWorkPapers/Examples/ChallengeBridge.lean
      sorry_count: 0
      axioms: ["propext", "Classical.choice", "Quot.sound"]
      comparator_config: lean/config.json

fidelity:
  divergences: >-
    (1) ordinary_forces_card_ge_six adds [Fintype H]; the paper's Theorem 4.1
    states |H| >= 6 for any H, which for infinite H is carried by the
    embedding theorem. (2) twelve_unique_kernel is stated on Fin 3 x Fin 2
    with Mathlib's product Heyting structure, not on the literal divisor
    lattice of 12; the order-isomorphism Div12 = Fin 3 x Fin 2 is
    kernel-checked in the library (div12OrderIsoChains) but is not part of
    the challenge statement, because Mathlib has no Heyting structure on
    the divisors of 12 to state it against. (3) OrdinaryElement is the
    two-clause form (not not a != a, not a != bot); the paper's section 2.1
    uses the three-clause form with a != bot added. The forms are equivalent
    (a = bot is regular); the equivalence is kernel-checked in
    lean/ChallengeChecks.lean (ordinaryElement_iff_three_clause). (4)
    FourRegionsInhabited lists the regions in the order I, D, E, R rather
    than the paper's I, R, E, D. (5) rnLadder's rung indexing follows the
    paper's section 2.2; indexing conventions in the literature differ and
    no rung-by-rung correspondence with Nishimura 1960 is claimed; the
    challenge's normal-form statement is indexing-independent because
    lean/ChallengeChecks.lean (rnLadder_generated) checks the converse
    inclusion, making it a two-sided characterization of the generated set.
    Closed 2026-10-12: ordinary_gives_z6_embedding was previously the
    existential "some order-embedding Fin 3 x Fin 2 -> H exists"; it now
    states that the paper's explicit map z6Landmarks g (bot, g, not g,
    not not g, g or not g, top, in divisor order 1, 2, 3, 4, 6, 12)
    preserves and reflects order, matching Theorem 4.2.

review:
  status: agent-reviewed
  reviewers:
    - "Chris Brink (human author; not a Lean reader): compared each challenge statement to the paper's theorem wording using an agent-prepared side-by-side, with the deviations disclosed under fidelity.divergences; did not review proofs"
    - "Independent AI model (cross-model pre-audit, 2026-07-12): OrdinaryElement vs Citkin's definition, redundancy of the compl constructor, non-bot guards in FourRegionsInhabited, rnLadder rungs 5-6"
  notes: >-
    No human Lean expert has reviewed the challenge statements. External
    review was requested in Lean Zulip #AI-authored-projects (2026-07) and
    remains open. Comparator certifies that Solution proves the exact
    Challenge statements with the three standard axioms; it cannot certify
    that Challenge.lean says what the paper says. That gap is the one this
    record is honest about. 2026-10-12: the human author, who does not read
    Lean, compared each of the six challenge statements to the paper's
    theorem wording (Theorems 3.2, 5.1, 5.2, 4.1, 4.2, 8.1(4)) using a
    side-by-side prepared by the agent, which also stated the deviations;
    the deviations are recorded under fidelity.divergences. Of the three
    weakenings found, the Z6 embedding (Theorem 4.2) was closed the same
    day by restating it on the paper's explicit map; the finite-only
    cardinality bound (1) and the Fin 3 x Fin 2 domain (2) stand as
    disclosed. The equivalences the review relied on are kernel-checked in
    lean/ChallengeChecks.lean, built in CI. Axioms re-audited
    the same day with #print axioms against a fresh build: as listed per
    result above; no sorryAx, no Lean.ofReduceBool. CI status: the
    comparator workflow passed at 73173a3 (2026-07-13) and failed at the
    "Run comparator" step on every run from d5dca50 (2026-07-29) through
    7b7763b (2026-10-12), the Lean build step passing each time. Root
    cause, from the run logs: the one unpinned input, landrun, merged an
    upgrade to urfave/cli v3 on 2026-07-22 whose parser drops the bare "--"
    that comparator uses to separate the module from the declaration names
    in its lean4export call, so lean4export read the theorem names as
    module names and aborted before any checking ("unknown module prefix
    'four_regions_iff_ordinary'"). No Lean content was ever at fault. The
    first repin (f33bea3, 2026-10-12) chose a commit that was not main's
    July tip and failed the same way; the second (5cf1aa9, same day) pins
    the last urfave/cli v2 commit and passes. See
    verification.last_passing_comparator_run for the verification of
    record, which covers the strengthened Z6 statement.

alignment:
  namespace: FalseWork.Lattice
  statements:
    - source: "Prop. 3.1 four-region partition"
      lean: FalseWork.Lattice.lattice_four_position_partition
      module: lean/FalseWorkPapers/Lattice/FourPositionLattice.lean
      status: proved
      note: "axioms: propext, Classical.choice, Quot.sound"
    - source: "Thm 3.2 non-degeneracy criterion"
      lean: FalseWork.Lattice.allFourCellsInhabited_iff
      module: lean/FalseWorkPapers/Examples/NishimuraKernelLaw.lean
      status: proved
      note: "axioms: propext; challenge name four_regions_iff_ordinary"
    - source: "Cor. 3.3 Boolean / Glivenko collapse"
      lean: FalseWork.Lattice.boolean_no_kernel, FalseWork.Lattice.glivenko_collapse
      module: lean/FalseWorkPapers/Examples/GlivenkoCollapse.lean
      status: proved
      note: "axioms: propext"
    - source: "Cor. 3.4 dense-bottom"
      lean: FalseWork.Lattice.no_ordinary_of_least_nonzero
      module: lean/FalseWorkPapers/Examples/LadderCore.lean
      status: proved
      note: "axioms: propext, Classical.choice, Quot.sound"
    - source: "Thm 4.1 six-element threshold"
      lean: FalseWork.Lattice.ordinary_card_ge_six, FalseWork.Lattice.allFourCells_card_ge_six
      module: lean/FalseWorkPapers/Examples/LadderCore.lean
      status: proved
      note: "axioms: propext, Classical.choice, Quot.sound; challenge name ordinary_forces_card_ge_six"
    - source: "Thm 4.2 Z6 order-embedding"
      lean: FalseWork.Lattice.div12OrderEmbedding
      module: lean/FalseWorkPapers/Examples/LadderCore.lean
      status: proved
      note: "axioms: propext; challenge name ordinary_gives_z6_embedding (explicit map z6Landmarks, order preserved and reflected)"
    - source: "Thm 5.1 Nishimura normal form"
      lean: FalseWork.Lattice.generatedBy_isLadderValue
      module: lean/FalseWorkPapers/Examples/NishimuraNormalForm.lean
      status: proved
      note: "axioms: propext, Quot.sound; challenge name nishimura_normal_form"
    - source: "Thm 5.2 uniqueness of the ordinary element"
      lean: FalseWork.Lattice.nishimura_ordinary_unique, FalseWork.Lattice.nishimura_kernel_unique_of_generated
      module: lean/FalseWorkPapers/Examples/NishimuraKernelLaw.lean
      status: proved
      note: "axioms: propext, Quot.sound; challenge name unique_ordinary_element"
    - source: "Cor. 5.3 unique generator at Z6"
      lean: FalseWork.Lattice.Examples.Div12.generator_unique
      module: lean/FalseWorkPapers/Examples/LadderCore.lean
      status: proved
      note: "axioms: propext, Quot.sound"
    - source: "Rem. 5.4 subalgebra-upgrade failure"
      lean: FalseWork.Lattice.Examples.nishimuraTerm_himp_diagonal
      module: lean/FalseWorkPapers/Examples/NishimuraNormalForm.lean
      status: proved
      note: "axioms: propext, Quot.sound"
    - source: "Rem. 5.5 substitution monoid End(Z6) = Z6"
      lean: FalseWork.Lattice.heytingHom_map_nishimuraTerm, FalseWork.Lattice.heytingHom_ext_of_generated, FalseWork.Lattice.endo_eq_id_iff_fixes_kernel, FalseWork.Lattice.Examples.Div12.endo_bijection, FalseWork.Lattice.Examples.Div12.substHom_comp, FalseWork.Lattice.Examples.Div12.subst_cube
      module: lean/FalseWorkPapers/Examples/SubstitutionMonoid.lean
      status: proved
      note: "axioms: propext, Quot.sound"
    - source: "Thm 6.1 H8 converse counterexample"
      lean: FalseWork.Lattice.Examples.unique_ordinary_converse_false, FalseWork.Lattice.Examples.h8_ladder_core
      module: lean/FalseWorkPapers/Examples/UniqueOrdinaryConverse.lean
      status: proved
      note: "axioms: propext, Quot.sound; minimality of H8 is script-level, see known_gaps"
    - source: "Prop. 6.2 dense-filter characterization"
      lean: FalseWork.Lattice.Examples.unique_ordinary_dense_iff
      module: lean/FalseWorkPapers/Examples/UniqueOrdinaryConverse.lean
      status: proved
      note: "axioms: propext, Quot.sound"
    - source: "Thm 7.1 Div12 one-generated by the tritone"
      lean: FalseWork.Lattice.Examples.Div12.one_generated_by_tritone, FalseWork.Lattice.Examples.Div12.tritone_generates, FalseWork.Lattice.Examples.Div12.kernel_unique
      module: lean/FalseWorkPapers/Examples/NishimuraTruncations.lean
      status: proved
      note: >-
        axioms: propext, Quot.sound. The abstract identification Div12 = Z6
        in the paper's prose invokes Citkin 2024 Theorem 6 (uniqueness of the
        one-generated algebra of each cardinality); that step is a
        literature dependency, not kernel-checked.
    - source: "Thm 8.1 p^2 q law for two primes; unique kernel of C3 x C2 at (1,0)"
      lean: FalseWork.Lattice.total_no_kernel, FalseWork.Lattice.Examples.chainProd_kernel_exists_iff, FalseWork.Lattice.Examples.chainProd_kernel_unique_iff, FalseWork.Lattice.Examples.why_twelve, FalseWork.Lattice.Examples.twelve_kernel_unique
      module: lean/FalseWorkPapers/Examples/WhyTwelve.lean
      status: proved
      note: "axioms: propext, Classical.choice, Quot.sound; challenge name twelve_unique_kernel"
    - source: "Thm 8.2 general k-prime law and count formula"
      lean: FalseWork.Lattice.Examples.piChain_kernel_iff, FalseWork.Lattice.Examples.piChain_kernel_exists_iff, FalseWork.Lattice.Examples.piChain_kernel_unique_iff, FalseWork.Lattice.Examples.piChain_kernel_card
      module: lean/FalseWorkPapers/Examples/WhyTwelveGeneral.lean
      status: proved
      note: "axioms: propext, Classical.choice, Quot.sound"
    - source: "Thm 6.1 minimality of H8 (eight is the least cardinality)"
      lean: ""
      module: ""
      status: not-formalized
      note: "script-level enumeration via Birkhoff duality, cross-checked against OEIS A006982; flagged in the paper, section 6"
    - source: "Divisor lattice of n = product of one chain per prime (general n)"
      lean: ""
      module: ""
      status: literature-dependency
      note: "cited, not formalized; the n = 12 instance is kernel-checked (div12OrderIsoChains)"

acknowledgements: >-
  Alex Citkin for the prior-art correspondence (June 2026). Mathlib for the
  HeytingAlgebra API. leanprover/comparator (Lean FRO) for the
  statement-match check.

# ---------------------------------------------------------------------------
# Extra keys (outside the v0.4 template; permitted by the schema).
# ---------------------------------------------------------------------------

verification:
  challenge_file: lean/Challenge.lean
  solution_file: lean/Solution.lean
  solution_module: Solution
  bridge_file: lean/FalseWorkPapers/Examples/ChallengeBridge.lean
  comparator_config: lean/config.json
  ci_workflow: .github/workflows/comparator.yml
  permitted_axioms: [propext, Classical.choice, Quot.sound]
  native_decide_in_scope: false
  audit_lines: lean/FalseWorkPapers/Examples/HeytingTypeInstance.lean
  last_passing_comparator_run: "2026-10-12, commit 5cf1aa9, run 38324798569: Lean default kernel accepts the solution (nanoda disabled); previous pass 2026-07-13, commit 73173a3"
  comparator_failure_window: "2026-07-29 (d5dca50) to 2026-10-12 (7b7763b): landrun/urfave-cli v3 dropped comparator's '--' separator; no Lean content involved"
  statement_checks: lean/ChallengeChecks.lean  # lean_lib ChallengeChecks, built in CI

# The files whose contents the claims above cover (the paper's section-10
# audit table). Two files elsewhere under lean/FalseWorkPapers/Examples/
# (MusicKernelZMod12Accum.lean, PythagoreanCommaConvergents.lean) belong to
# the music-kernel track, use native_decide, and are outside this paper's
# claims and outside comparator scope. The additional tracks below are
# likewise outside this scope.
scope_files:
  - lean/FalseWorkPapers/Examples/GlivenkoCollapse.lean
  - lean/FalseWorkPapers/Examples/HeytingTypeInstance.lean
  - lean/FalseWorkPapers/Examples/LadderCore.lean
  - lean/FalseWorkPapers/Examples/NishimuraKernelLaw.lean
  - lean/FalseWorkPapers/Examples/NishimuraNormalForm.lean
  - lean/FalseWorkPapers/Examples/NishimuraTruncations.lean
  - lean/FalseWorkPapers/Examples/SubstitutionMonoid.lean
  - lean/FalseWorkPapers/Examples/UniqueOrdinaryConverse.lean
  - lean/FalseWorkPapers/Examples/WhyTwelve.lean
  - lean/FalseWorkPapers/Examples/WhyTwelveGeneral.lean
  - lean/FalseWorkPapers/Lattice/FourPositionLattice.lean
  - lean/FalseWorkPapers/Examples/ChallengeBridge.lean

known_gaps:
  - >-
    Minimality of the H8 counterexample (eight is the least cardinality) is
    established by script-level enumeration, not in Lean; flagged in the
    paper (section 6).
  - >-
    The classical structure theorem "divisor lattice of n = product of one
    chain per prime" is cited, not formalized, for general n; the n = 12
    instance is kernel-checked (div12OrderIsoChains).
  - >-
    Div12 = Z6 as an abstract isomorphism rests on Citkin 2024 Theorem 6;
    the Lean establishes one-generation of Div12 by the tritone and the
    kernel/embedding facts directly.

additional_tracks:
  - name: opposition-figure-and-bridge
    title: "The opened square: bridge theorem + opposition figure (Lean 4)"
    paper: preprints/opposition-figure/paper.md
    short_description: >-
      Welds the topos stack (four-position partition) to the lattice stack
      (ordinary elements): the partition at Y is non-degenerate iff the
      kernel image is ordinary in Sub(D Y), and ordinary kernels force the
      Z6 order-embedding (OrdinaryKernel.lean). Formalizes the opposition
      figure: the six landmarks bot, not-a, a, not-not-a, a-or-not-a, top
      are pairwise distinct iff a is ordinary (T1); classical/regular/dense
      collapse laws; the skeleton theorem (each middle landmark inhabits its
      partition cell); on Div12 at the tritone the figure is the identity;
      Blanche's 1966 hexagon is not order-isomorphic to Z6 (T2)
      (OppositionFigure.lean). The Aristotelian relation profile of the
      opened square (OppositionRelations.lean): at an ordinary a the
      negation pair a, not-a is contrary and never contradictory (the
      element-local form of Beziau 2003); three strict subalternations;
      the E-I and I-U pairs split on the Stone identity at a (weak excluded
      middle), contradictory + subcontrary if it holds (as on Z6 at the
      tritone, proved computably), contrary + unconnected (Demey-Smessaert's
      fourth relation) if it fails.
    files:
      - lean/FalseWorkPapers/Positions/OrdinaryKernel.lean
      - lean/FalseWorkPapers/Examples/OppositionFigure.lean
      - lean/FalseWorkPapers/Examples/OppositionRelations.lean
    sorry_count: 0
    native_decide: false
    axioms: at most propext, Classical.choice, Quot.sound (per-theorem audit table in the paper, section 10)
    comparator: none (not in the challenge module)
    review_record:
      - >-
        BlancheHexagon cover table vs. Blanche (1966): reviewed 2026-07-29
        (AI web-research under direction) against three independent
        specialist descriptions (Beziau, "The metalogical hexagon of
        opposition," Argumentos 2013, citing Blanche 1966 directly;
        Dubois-Prade-Rico, AMAI 2015; standard references). All six
        entailment edges, both incomparability triangles, and the three
        contradictory pairs match. Residual: the 1966 French primary text
        was not consulted (no accessible copy).
      - >-
        Intuitionistic-square chapters: reviewed 2026-07-29. Records
        correction: only one such chapter is in the 2012 volume (Meles,
        "No Group of Opposition for Constructive Logics," pp. 201-217,
        group-theoretic); the other is Vidal-Rosset, "The Exact
        Intuitionistic Meaning of the Square of Opposition," in the 2017
        volume The Square of Opposition: A Cornerstone of Thought
        (pp. 291-303, prover-driven). Neither works at the algebra-element
        level or states the ordinariness equivalence; targeted searches for
        square + Rieger-Nishimura and square + regular/dense elements came
        back empty. Residual: full chapter texts paywalled; review rests on
        abstracts, the authors' own congress summaries, and citing
        literature, all concordant.
  - name: aperture-and-falsework
    title: "Aperture closed form and the falsework inequality (Lean 4)"
    short_description: >-
      Kernel-checked results outside the ordinary-elements paper: the
      aperture closed form at every arity (aperture_closed_form_pi,
      Lattice/ApertureClosedFormPi.lean), the falsework inequality
      (falsework_inequality, Lattice/FalseworkInequality.lean), the
      morphism-level four-position partition (four_position_partition,
      Positions/Partition.lean). Each has its own paper and audit table;
      none is in the challenge module.
    files:
      - lean/FalseWorkPapers/Lattice/ApertureClosedFormPi.lean
      - lean/FalseWorkPapers/Lattice/FalseworkInequality.lean
      - lean/FalseWorkPapers/Positions/Partition.lean
    sorry_count: 0
    native_decide: false
    comparator: none (not in the challenge module)